add important revision notes

[cdsspec-compiler.git] / notes / nondeterm-spec.txt

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
new file mode 100644 (file)
index 0000000..f76c46c
--- /dev/null
+++ b/notes/nondeterm-spec.txt
@@ -0,0 +1,93 @@
+Modification to the current specifications.
+1. Local State --- Beside of having one global sequential state (the one that we
+had in the old approach), we also allow each method call to have a local state.
+This local state is the accumulative side effects of the subset of method calls
+that happen before the current method call. 
+
+To evaluate the local state of each method call, an obvious approach is
+calculate from the initial state for each. An optimization we can make here is
+that we can start to evaluate the state from the most recent common parent. And
+such a state is only evaluated when needed.
+
+2. CONCURRENT --- an operation that extracts all the methods that are executing
+"concurrently" with the current method.
+"before" the current method.
+
+3. PREV --- an operation that extracts all the methods that execute right
+
+1. The register file examples.
+----------   Interfae   ----------
+void init(atomic_int &loc, int initial);
+int load(atomic_int &loc);
+void store(atomic_int &loc, int val);
+----------   Interfae   ----------
+
+a. The SC atomics --- the classic linearizability approach
+b. The ordered-store acq/rel atomics
+We basically allow a load operation to read form any store that this does not happen
+before
+
+----------   Specification   ----------
+// Store to the same location should conflict
+@Commutativity: Store <-> Store(Store.loc != Store.loc)
+@Commutativity: Store <-> Load
+@Commutativity: Load <-> Load
+
+@DeclareVar: int x;
+@InitVar: x = 0;
+
+@Interface: Store
+@SideEffect:
+       x = val;
+
+@Interface: Load
+@SideEffect:
+@PostCondition:
+       __RET__ == x ||
+       {Last.Store(_M.loc == loc)}
+
+
+
+c. The C/C++ atomics
+
+
+d. The C/C++ normal memory accesses
+- Use the admissibility requirement, then the classic linearizability approach
+on the admissible executions
+
+
+A good example to simulate a queue data structure is as follows.
+Suppose we have a special structure
+typedef struct Q {
+       atomic_int x;
+       atomic_int y;
+} Q;
+
+, and we have two interface on Q, read() and write(), where the write and read
+method calls are synchronized by themselves, and they have to read and write the
+x and y fields in turn.
+
+
+----------------------------------------------------------------------------------------
+We also need to think about the non-ordered queue.
+
+####
+Combiming Data Structures --- 
+For example, a queue, a -hb->c, b -hb-> e.
+
+// T1
+enq(1) -> {1} - {$}    // a
+enq(2) -> {1, 2} - {$}   // b
+
+// T2
+deq(1) -> {$} - {1}   // c
+deq($) -> {$} - {1}   // d
+
+// State before this method  
+JOIN ({1, 2} - {$}, {$} - {1}) = {2} - {1}
+deq(2) -> {$} - {1, 2}
+
+
+
+
+