Choice (ALTing) over Multiway Synchronisations

This contains a collection of occam-pi and FDR scripts implementing and analysing algorithms for performing ALT (external choice) operations over multiple BARRIERs (multiway synchronisation events).

No guarantees are made (yet) about correctness.

All versions are archived here: <name>-<version>-<revision>, where <version> indicates an algorithmic change and <revision> indicates minor corrections or documentation changes.  Only the latest <revision> of a particular <name>-<version> is (normally) relevant.

The two-phase commit protocol negotiates a decision between n customer processes and m multiway sync processes.  The one-phase oracle delivers decisions made by a single process to n customer processes.  The latter is much simpler than the former and should be much faster - for example, the serialisation means that no undoing ("collapsing") of just-missed synchronisations is necessary.  The idea for this was pointed out by Ian Marshall when we tried explaining the two-phase commit to him.  If correct, this opens the way to a reasonably efficient implementation for multiway sync guards in occam-pi.

Two-phase commit protocol

mm-sync-0-0.occ (initial version - experimental - not compileable)
mm-sync-1-0.occ (earlier version - uses SEMAPHOREs for RAP locking)
mm-sync-2-0.occ (exploits nested CLAIM over an array of channel-ends for RAP locking)

mm-sync-0-0.csp (first draft - contains low-level errors)
mm-sync-0-1.csp (earlier version - contains low-level errors)
mm-sync-0-2.csp (earlier version - older documentation)
mm-sync-0-3.csp (FDR script - corresponds to the above occam-pi implementations)
mm-sync-0-4.csp (FDR script - minor corrections to the version 0.3 above)

One-phase (sequential) oracle

mm-sync-oracle-0-0.occ (initial version - very simple - obviously correct?)
mm-sync-oracle-1-0.occ (simple optimisation - not sure worthwhile?)

mm-sync-oracle-0-0.csp (FDR script - refined by the above occam-pi implementations)
mm-sync-oracle-0-1.csp (FDR script - flattened version of version 0.0 above)

Implementing SYNC guards for occam-pi

sync-guards-0-0.txt (technical report - initial thoughts)

Peter Welch.