Changes between Version 2 and Version 3 of Language

Timestamp:

05/17/23 21:16:09 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -229 +229 @@
 Let `s1` and `s2` be expressions of type `$scope`. The following are all CIVL-C expressions of boolean type:
 
-* `s1 == s2`. Holds iff `s1` and `s2` refer to the same dynamic scope.
-* `s1 != s2`. Holds iff `s1` and `s2` refer to different dynamic scopes.
-* `s1 <= s2`. Holds iff `s1` is equal to or a descendant of `s2`, i.e., `s1` is equal to or contained in `s2`.
-* `s1 < s2`. Holds iff `s1` is a strict descendant of `s2`, i.e., `s1` is contained in `s2` and is not equal to `s2`.
-* `s1 > s2`. Equivalent to `s2 < s1`.
-* `s1 >= s2`. Equivalent to `s2 <= s1`.
+* `s1 == s2` holds iff `s1` and `s2` refer to the same dynamic scope.
+* `s1 != s2` holds iff `s1` and `s2` refer to different dynamic scopes.
+* `s1 <= s2` holds iff `s1` is equal to or a descendant of `s2`, i.e., `s1` is equal to or contained in `s2`.
+* `s1 < s2` holds iff `s1` is a strict descendant of `s2`, i.e., `s1` is contained in `s2` and is not equal to `s2`.
+* `s1 > s2` is equivalent to `s2 < s1`.
+* `s1 >= s2` is equivalent to `s2 <= s1`.
 
 Each of these expressions is erroneous if `s1` or `s2` is undefined.  This error is reported by the model checker.
@@ -244 +244 @@
 == Statements
 
-
 === `$atomic`
 
+An ''atomic block'' is a statement of the form
+{{{
+$atomic {
+  stmt1;
+  stmt2;
+  ...
+}
+}}}
+and indicates that the statements comprising the block should be executed without the intervention of other processes.
+
+More precisely, there is a global atomic lock which is initially free.
+A process attempting to execute an atomic block will wait until the atomic lock becomes free, i.e., no other process is inside an atomic block.
+The process must also wait until the guard of the atomic block holds; this means that the first statement in the block is enabled.
+Once the atomic lock is free and the guard holds, the atomic block becomes enabled and the process may enter the atomic block.
+The process may not necessarily enter the atomic block as soon as these conditions hold, because some other enabled process may be scheduled first.
+In fact, some other process may obtain the atomic lock.
+But if the enabling conditions hold and this process is scheduled, it will obtain the atomic lock and begin executing the statements of the atomic block without other processes executing.
+Upon reaching the end of the atomic block, the process releases the atomic lock and exits the block.
+
+There is an exception to atomicity: if the process inside the atomic block executes a `$yield` statement, it releases the atomic lock.
+This allows other processes to execute, and even obtain the lock.
+At any point at which the atomic lock is free and the first statement following the `$yield` is enabled, the original process may re-obtain the atomic lock and continue executing its block atomically.
+
+If a statement inside an atomic block blocks, so that the process executing the atomic block has no enabled statement, execution deadlocks. 
+The exception to this rule is that the first statement in the atomic block, and the first statement after a `$yield`, as described above, may block, without necessarily causing deadlock.
+
+Atomic blocks may be nested.
+Hence the atomic lock is held with a certain multiplicity.
+Each time the process enters an atomic block, the multiplicity is incremented.
+Each time it leaves an atomic block, the multiplicity is decremented.
+When the multiplicity hits 0, the atomic lock is released.
+Execution of a `$yield` does not change the multiplicity; the process releases the lock but maintains the multiplicity, so that when the lock is re-obtained, the original multiplicity is still in place.
+
 === `$choose`