Changes between Version 25 and Version 26 of OpenMPTransformation

Timestamp:

04/25/14 09:24:47 (12 years ago)

Author:

siegel

Comment:

--

OpenMPTransformation

@@ -40 +40 @@
 == Helper primitives ==
 
-`$int_iter` is a handle type for an iterator of integers.
-
-{{{
-/* Tells whether the integer iterator has any more elements */
-_Bool $int_iter_hasNext($int_iter iter);
-
-/* Returns the next element in the iterator (and updates the iterator) */
-int $int_iter_next($int_iter iter);
-}}}
+None.
 
 == Modeling shared variables ==
 
-For each shared variable `v` introduce a second variable `v_state`.  The type of `v_state` is obtained from the type of `v` by replacing all primitive types (leaf nodes in the type tree) by `int`.  Initially all these ints are -1.
+For each shared variable `v` introduce a second variable `v_state`.  The type of `v_state` is obtained from the type of `v` by replacing all primitive types (leaf nodes in the type tree) by `int`.  Initially all these ints are -1.  Both variables are declared in the same, shared, scope.
+
+In addition to the shared variable v, each thread has its own local copy named `_v`, declared in thread private scope.   It has the same type as `v`.
+
+Protocols for reads, writes, and flushes:
 
 A write to (some part of) the shared variable by thread tid:
-* if the state value is -1, set it to tid, then do the write
-* if the state value is tid, do the write
-* else report a data race.
+* if the state value is -1, do the write to the local copy and set the state value to tid.  Now thread tid is the "owner" of that memory unit.
+* if the state value is tid, do the write to the local copy.
+* else report a memory model error: you are attempting to write to a variable when some other thread has un-flushed writes to the same variable.  The other thread should flush, then you should flush, before doing this write.
 
 A read from (some part of) the shared variable by thread tid:
-* if the state value is -1 or tid, do the read
-* else report a data race.
+* if the state value is -1, read your local copy and compare it to the global copy.  If they differ, report a memory model error: some other thread has modified the variable and flushed, but you did not flush before performing the read. (If you had flushed, your local copy and the shared copy would be equal.)
+* if the state value is tid, read your local copy.
+* else report a memory model error: you are reading from a variable when another thread has un-flushed writes to that variable.  The other thread should flush, and then you should flush, before doing this read.
 
 Translating `flush`of (some part of) the shared variable by thread tid:
-* if the state value is -1: no-op
-* if the state value is tid: set it to -1
-* else: some other thread has some write to the variable which it hasn't flushed.  But this thread has not done any writes to that variable (since it last flushed).  This is a no-op.
-
-Function
+* if the state value is -1: copy the global value to your local copy of the variable.
+* if the state value is tid: copy your local value to the global copy of the variable and set the state value to -1.
+* else: report a memory model error, since you are doing a flush when some other thread has un-flushed writes to the variable.  The other thread should flush first.
+
+We will implement the following function, which is implicit in many of the OpenMP constructs:
 {{{
   barrier_and_flush();
 }}}
-does a barrier on `_barrier` and a flush on all shared variables.
-
-PROBLEM: the above does not seem to guarantee that both the writing and reading thread do flushes.  According to the Standard, events should follow this order: thread 1 writes , thread 1 flushed, thread 2 flushes, thread 2 reads.     The protocol above doesn't require the thread 2 flush.
-
+It does a barrier on `_barrier` and a flush on all shared variables.  After this completes, all local copies will agree with each other and with the shared copy of the variable, and all state variables will be -1.
 
 == Modeling worksharing state ==