Support PlusCal either statement

[minhnhdo]

The either statement executes a random non-blocking clause. We could implement this with select in Go, but it's difficult to get it into a format where select works.

Original issue: https://bitbucket.org/whiteoutblackout/pgo/issues/39/support-pluscal-either-statement

[minhnhdo]

The select solution might first evaluate whether the step can block, then send a value to some channel if it doesn't. The select cases would pull from each of the channels. If await statements must occur at the top of steps, then the test corresponds to testing just the await.

Original comment: https://bitbucket.org/whiteoutblackout/pgo/issues/39/support-pluscal-either-statement#comment-39332942

[minhnhdo]

An either statement has the following form.

either statements
    or statements
    or statements

Like #10, either statements have to be the first in an atomic step. Furthermore, if a subblock in an either statement contains an await statement, that await statement has to be the first in the subblock.

With the above restrictions, an either statement has the following form.

label: either await x
              doThingsWithX
           or await y
              doThingsWithY
           or doStuff
           or doOtherStuff

The above either statement will be translated into the following.

// Global variables
var (
    cx = make(chan bool)
    cy = make(chan bool)
)

func waitForX() {
    for {
        lock()
        if x {
            break
        }
        unlock()
        yield()
    }
    // still locked
    cx <- true
}

func waitForY() {
    for {
        lock()
        if y {
            break
        }
        unlock()
        yield()
    }
    // still locked
    cy <- true
}

func process(self string) {
    go waitForX()
    go waitForY()
    select {
    case <-cx:
        doThingsWithX
        unlock()
    case <-cy:
        doThingsWithY
        unlock()
    default:
        switch rand() % 2 {
        case 0:
            doStuff
        default: // case 1
            doOtherStuff
        }
    }
}

[minhnhdo]

The above scheme still need to deal with leaking goroutines and channels.