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) ...