Changes between Version 26 and Version 27 of Language

Timestamp:

05/19/23 20:51:05 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -605 +605 @@
 In this program, the threads write to `x` within a local region.  This program has only one execution: first thread 1 executes the complete local region, then thread 2 executes the complete local region.  Running `civl verify` on this code yields "all properties hold".
 
+==== Example
+
+The code
+{{{
+  $local_start();
+  ...A...
+  $local_end();
+  $local_start();
+  ...B...
+  $local_end()
+}
+int main() {
+  $parfor (int i:1..2) thread(i);
+}
+}}}
+also has only one execution.
+Thread 1 will execute local block A and then release the atomic lock.
+But at that point, thread 1 will again be the thread of lowest PID at a `$local_start()` and therefore will be the only enabled thread.
+It will execute local block B, and only then will thread 2 execute.
+The code above is equivalent to
+{{{
+ $local_start();
+  ...A...
+  ...B...
+  $local_end()
+}
+int main() {
+  $parfor (int i:1..2) thread(i);
+}
+}}}
+
 ==== Use of `$yield` within a local region
 
@@ -612 +643 @@
 then ''t'' may return from the `$yield` call and re-obtain the atomic lock.
 
+Note that a thread waiting to return from a `$yield` has no special priority, even if that `$yield` is inside at local region.
+Only `$local_start` grants a thread a special priority.
+This is illustrated in the following example.
+
+==== Example
+
+
+
 === Heap memory allocation: `$malloc` and `$free`