-1. Global state: We allow users to specify a single global state so that when we
-want to execute the sequential replay (execute the sequential order), the whole
-process is similar to executing an sequential program. Such a global state is
-similiar to the internal state of a sequential data structure. We also have this
-in our old version (the rejection of PLDI'16). As an analogy to the cache-memory
-model, the global state we define here is similar to the main memory in the
-sense that there does not exist a real total order to all memory accesses, but
-to some degree (with the non-deterministic specifications) we can have an
-illution that there is some total order.
-
-2. Local State: Beside of having one global state (the one that we have 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. As an analogy to the cache-memory model, the
-local state we define here is similar to cache, a local state is local to the
-sense that the current method call must have seen those effects. The main goal
-of having this is to support tighter non-deterministic specifications.
-
-To evaluate the local state of each method call, an obvious approach is to
+Previously, we keep a sequential state throughout the process of executing the
+sequential history. In our model, we keep a state local to each method call.
+Conceptually, this state is the accumulative side effects of the subset of
+method calls that happen before the current method call.
+
+To evaluate the state of each method call, an obvious approach is to