+/// Ordering point specification
+@OPDefine: condition // If the specified condition satisfied, the atomic
+ // operation right before is an ordering point
+
+@PotentialOP(Label): condition // If the specified condition satisfied, the
+ // atomic operation right before is a potential
+ // ordering point, and we label it with a tag
+
+@OPCheck(Label): condition // If the specified condition satisfied, the
+ // potential ordering point defined earlier with the
+ // same tag becomes an ordering point
+
+@OPClear: condition // If the specified condition satisfied, all the
+ // ordering points and potential ordering points will be
+ // cleared
+
+@OPClearDefine: condition // If the specified condition satisfied, all the
+ // ordering points and potential ordering points will
+ // be cleared, and the atomic operation right before
+ // becomes an ordering point. This is a syntax sugar
+ // as the combination of an "OPClear" and "OPDefine"
+ // statement
+
+
+1. The register examples: Basically, we can think of registers as the cache on a
+memory system. The effect of a load or store basically tells us what the current
+value in the cache line is, and a load can read from values that can be
+potentially in the cache --- either one of the concurrent store update the cache
+or it inherites one of the the previous local state in the execution graph.
+
+---------- 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 RA (release/acquire) C/C++ atomics
+// For RA atomics, a load must read its value from a store that happens before
+// it.
+---------- Specification ----------
+@DeclareVar: int x;
+@InitVar: x = 0;
+
+@Interface: Store
+@SideEffect: LOCAL(x) = val;
+void store(int *loc, int val);
+
+@Interface: Load
+@PreCondition:
+ Size(Subset(PREV, LOCAL(x) == RET)) > 0;
+@SideEffect: LOCAL(x) = RET;
+int load(int *loc);
+
+c. The C/C++ atomics (a slightly loose specification)
+// Actually, any concurrent data structures that rely modification-order to be
+// correct would not have a precicely tight specification under our model, and
+// C/C++ relaxed atomics is an example. See the following read-read coherence
+// example.
+
+// T1 // T2
+x = 1; x = 2;
+
+// T3
+r1 = x; // r1 == 1
+r2 = x; // r2 == 2
+r3 = x; // r3 == 1
+
+Our model cannot prevent such a case from happening. However, we can still have
+a slightly loose specification which basically states that a load can read from
+any store that either immediately happens before it or concurrently executes.
+
+