Tressa: Claiming the Future

Unlike sequential programs, concurrent programs have to account for interference on shared variables. Static verification of a desired property for such programs crucially depends on precisely asserting the conditions for interference. In a static proof system, in addition to program variables, auxiliary (history) variables summarizing the past of the program execution are used in these assertions. Capable of expressing reachability only, assertions (and history variables) are not as useful in the proofs of programs using optimistic concurrency. Pessimistic implementations which allow access to shared data only after synchronization (e.g. locks) guarantee exclusivity; optimistic concurrency implementations which check for interference after shared data is accessed abandon exclusivity in favor of performance.