DistCompiler / pgo

PGo is a source to source compiler from Modular PlusCal specs into Go programs.
https://distcompiler.github.io/
Apache License 2.0
172 stars 13 forks source link

Support PlusCal await statement #10

Closed minhnhdo closed 6 years ago

minhnhdo commented 6 years ago

In PlusCal, await blocks an atomic step from executing until the condition is true. The following might be a way to implement await in Go:

Original issue: https://bitbucket.org/whiteoutblackout/pgo/issues/38/support-pluscal-await-statement

minhnhdo commented 6 years ago

After some discussion, we have agreed to put in the first restriction, i.e. await statements can only occur at the top of an atomic step.

Await statement

await exp;

will be translated into

for {
    lock
    if exp {
        break
    }
    unlock
    yield
}
// use variables
unlock

The yield statement in the above infinite loop is to invoke the Go scheduler.

Original comment: https://bitbucket.org/whiteoutblackout/pgo/issues/38/support-pluscal-await-statement#comment-42541651

minhnhdo commented 6 years ago

Fixed in 6a8a4a7ba5