Non-Atomic Variables

  var1: [t1 -> v1; t2 -> v2]

where var1 is the name of the variable, tx are timestamps, and vx are the values of the variable at those timestamps.

Note that t(n+1) must be greater than t(n)

Domains

Domains are separate spheres of execution. Each thread would have their own Domain, for instance.

Frontier

Domains have a frontier, which establishes which variables it can see at which timestamp.

  d1: [var1 -> t1; var2 -> t3; var3 -> t7]

where d1 is the name of the domain, varx are variable names, and tx are timestamps

If a variable is at tx, we can read any value for ty, y >= x. Aka we can read any later writes, but never any earlier states.

Updating frontiers

Non-atomic reads do not modify frontier

Non-atomic writes update var with new value, and update the timestamp in domain

Atomics

Atomics also have frontiers

  A1: v1 [var1 -> t1; var2 -> t5]

where A1 is the name of the atomic, v1 is the current value of the atomic, and the rest is the frontier of the atomic

Atomic Reads

The frontier of the atomic is merged into the frontier of the domain.

Example: TODO

Atomic Writes

Atomic value is updated, frontier of atomic and domain are merged and BOTH updated.

Example: TODO