This webpage contains Viper-encoded examples referenced in the paper "Automating Deductive Verification for Weak Memory Programs" See also the prototype tool.

RSL Spinlock Example

(RSLSpinlock) Encoding of Figure 7 Spinlock example from RSL paper

Release-Acquire Message-Passing

(RelAcqMsgPass) Encoding of Figure 8 message passing example from RSL paper

Fence-Based Double Message-Passing

(FencesDblMsgPass) Encoding of Figure 2 double message passing example from FSL paper

Fence-Based Double Message-Passing, Single Atomic Location

(FencesDblMsgPassSplit) Adaptation of program from Figure 2 of FSL paper (with CAS accesses), using a single atomic location and correspondingly more-complex invariant which must be split between threads

Fence-Based Double Message-Passing, Single Atomic Location, Invariant Rewriting

(FencesDblMsgPassAcqRewrite) Adaptation of program from Figure 2 example from FSL paper, using a single atomic location with invariant stated such that automatic handling of conjuncts doesn't suffice; exercises invariant rewriting support

Release-Acquire Double Message-Passing, Invariant Splitting

(RelAcqDblMsgPassSplit) Adaptation of program from Figure 2 of FSL paper, using Release/Acquire accesses, a single atomic location and correspondingly more-complex invariant which must be split between threads

Rust Reference Counter (Acquire/Release variant)

(RelAcqRustARCStronger) An adaptation of the Rust reference counting example from FSL++ paper ...

Rust Reference Counter (Fences variant)

(ARCStronger) An adaptation of the Rust reference counting example from FSL++ paper ...

Rust Reference Counter (original)

(ARCRelaxed) Encoding of original example from FSL++ paper, using same specs as previous example ...

Facebook Folly Reader-Writer spinlock code

(FollyRWSpinlock_err) Encoding of the core reader-lock and writer-lock functions from Facebook's open-source Folly library ...

Facebook Folly Reader-Writer spinlock (relacq)

(FollyRWSpinlock_err_mod) Encoding of the core reader-lock and writer-lock functions from Facebook's open-source Folly library, simplified to use only relacq accesses (see FollyRWSpinlock_err for the original) ...

Facebook Folly Reader-Writer spinlock code, two modified functions

(FollyRWSpinlockStronger) Encoding of the core reader-lock and writer-lock functions from Facebook's open-source Folly library ...

Facebook Folly Reader-Writer spinlock code (relacq), two modified functions

(FollyRWSpinlockStronger_mod) Encoding of the core reader-lock and writer-lock functions from Facebook's open-source Folly library, simplified to use only relacq accesses (see FollyRWSpinlockStronger for the original) ...