An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory

In the celebrated Godel Prize winning papers, Herlihy, Shavit, Saks and Zaharoglou gave topological characterization of waitfree computation. In this paper, we characterize waitfree communication logically. First, we give an intuitionistic epistemic logic K boolean OR for asynchronous communication. The semantics for the logic K boolean OR is an abstraction of Herlihy and Shavit's topological model. In the same way Kripke model for intuitionistic logic informally describes an agent increasing its knowledge over time, the semantics of K boolean OR describes multiple agents passing proofs around and developing their knowledge together. On top of the logic K boolean OR, we give an axiom type that characterizes sequential consistency on shared memory. The advantage of intuitionistic logic over classical logic then becomes apparent as the axioms for sequential consistency are meaning less for classical logic because they are classical tautologies. The axioms are similar to the axiom type for prelinearity (phi superset of psi) boolean OR (psi superset of phi). This similarity reflects the analogy between sequential consistency for shared memory scheduling and linearity for Kripke frames: both require total order on schedules or models. Finally, under sequential consistency, we give soundness and completeness between a set of logical formulas called waitfree assertions and a set of models called waitfree schedule models.