Specifying Concurrent and Synchronous Operations

I've spoken before on how to specify concurrent operations in a lock-free setting. The trick there is observations and effects, and safety is guaranteed when all possible ending states of all operations are valid starting states for each operation.

However, we need more than just this. Such a type system would be unable to certify the atomic snapshot protocol. To reason about this, we need two additional reasoning capabilities. First, we need to be able to reason about when an observation is made, or when an effect was caused. Secondly, we need to be able to infer this with arbitrary predicates over terms. For instance, in the atomic snapshot protocol, we need to be able to connect a memory tag with the time at which an operation occurred. In other words, if tag a is observed in one observation of a given location, and later, a tag b is observed such that a < b, then something effected that location in between the two observations. More importantly, if they are the same, then nothing affected the location.

Lastly, we need some means of reasoning about actual synchronous operations and their behavior. For instance, the synchronization barrier operation or lock/unlock operations imply certain timing behaviors between various threads. Barriers allow a thread to continue at some point after some other number of threads have executed a barrier wait.

Temporal Logic may be the key here, or at least a starting point. Temporal logic provides six different predicates on propositions. They are as follows:

• Fp (future): At some point in the future, p holds
• Pp (past): At some point in the past, p held
• Hp (henceforth): At all points in the future, p holds
• Gp (hitherto): At all points in the past, p held
• ☐p (always) = Gp ∧ p ∧ Hp: At all points in time, p holds
  
• ◇p (sometimes) = Pp ∨ p ∨ Fp: At some point in time, p holds

The best thing about temporal logic is that it is decidable (at least in some instances).

However, this logic alone isn't enough. Specifically, we need quantification over time quanta probably based on these predicates. Linearizability of terms in such a type system would then come down to identifying a specific time quantum which acts as the linearization point. For your basic lock-free algorithms, this is simply the time quantum of some operation in the term itself. For more complicated things, such as a lock-free garbage collector, then the "start collection" function specifies some point in future time (F) at which the heap is exchanged for an isomorphic superset of the observable locations at that point.

In any case, this is likely the way forward on this front.