Changes between Version 6 and Version 7 of Language

Timestamp:

05/17/23 22:43:27 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -363 +363 @@
 === Guarded commands: `$when`
 
+A guarded command is encoded in CIVL-C using a `$when` statement:
+{{{
+$when (expr) stmt;
+}}}
+All statements have a guard, either implicit or explicit. For most statements, the guard is ''true''. The `$when` statement allows one to attach an explicit guard to a statement.
+
+When `expr` is ''true'', the statement is enabled, otherwise it is disabled.
+A disabled statement is blocked—it will not be scheduled for execution.
+When it is enabled, it may execute by moving control to the `stmt` and executing the first atomic action in the `stmt`.
+If `stmt` itself has a non-trivial guard, the guard of the `$when` statement is the conjunction of the `expr` and the guard of `stmt`.
+
+The evaluation of `expr` and the first atomic action of `stmt` occur as a single atomic action.
+There is no guarantee that execution of `stmt` will continue atomically if it contains more than one atomic action, i.e., other processes may be scheduled.
+
+Examples:
+
+{{{
+$when (s>0) s--;
+}}}
+This will block until `s` is positive and then decrement `s`.
+The execution of `s--` is guaranteed to take place in an environment in which `s` is positive.
+
+{{{
+$when (s>0) { s--; t++; }
+}}}
+The execution of `s--` must happen when `s>0`, but between `s--` and `t++`, other processes may execute.
+
+{{{
+$when (s>0) $when (t>0) x=y*t;
+}}}
+This blocks until both `x` and `t` are positive then executes the assignment in that state.
+It is equivalent to
+{{{
+$when (s>0 && t>0) x=y*t;
+}}}
+
+
+The following statements are all equivalent:
+{{{
+$when (s>0) $atomic{ s--; t++; }
+$atomic{ $when(s>0); s--; t++; }
+$atomic{ $when(s>0) {s--; t++; } }
+}}}
+Each of these waits until `s` is positive, then from such a state, decrements `s` and increments `t` without the intervention of other processes.
 
 == Functions