Separation-based reasoning for deterministic channel-passing concurrent programs

Abstract

Tractable proof systems for concurrent processes are hard to achieve because of the non- deterministic interleaving of statements. This is particularly true when the scheduling of statements have an effect on the final state of the program, referred to as racy conditions. As a result, when we try to reason about concurrent programs, we have to consider all possible thread interleaving to accurately approximate the final result. Since, scalability is important we limit our reasoning to a subset of the concurrent programs that are race-free. By doing so we gain serialized reasoning, where examining one possible path will automatically encapsulate the other interleaving.