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). Two functions have been re-implemented with slightly less-efficient code whose correctness can, however, be captured by RSL-style atomic invariants.

//:: IgnoreFile(/carbon/issue/269/) // This example includes methods taken from the RWSpinlock implementation in the Facebook Folly library. // The two methods try_lock_shared_stronger unlock_and_lock_shared_stronger are reimplementations of the // original versions (found in the FollyRWSpinlock example), as the correctness arguments for the original // implementations cannot (we believe) be captured by the RSL logic features supported by our encoding. // For the former changed method, the code is potentially less efficient, but requires a less sophisticated // argument; for the latter, the new code is arguably *more* efficient than the original. // PLEASE NOTE: This version of the example is a variant which all access modes for atomic operations // are simply relacq. In our evaluation table, we inadvertently reported times for this version of the example. // The verification outcomes are identical, but the timings were somewhat faster; the correct timing for the // FollyRWSpinlockStronger example is around 25 seconds (i.e. comparable with our other advanced examples) // We will change this entry in the final version of the paper. // The version of the code using the corrected access modifiers is in the file FollwRWSpinlockStronger; this one // yields the times reported in the table. // Note that verification times via the web frontend are considerably longer than with the desktop application. // PART 1: translation of code // Q0 := (v < 0 ? false : ghostRef(ghost) && acc(ghost, leftover(v)) && realRef(bits) && acc(resource(bits), leftover(v)) && ghostRef(readsGhost) && acc(readsGhost, write - rd * (v/4))) // leftover(v) (v % 2 == 1 ? 0 : (secondBit(v) == 1 ? upgradeable - rd * (v/4) : 1 - rd * (v/4)))) // Lock(bits) := Rel(bits,Q0) && RMWAcq(bits,Q0) && Init(bits) && realRef(bits) // (see PART 2 of encoded file for further definitions) // we pass the real lock location and two ghost locations (ghost and readsGhost) around together, instead of encoding composite objects here. method try_lock(bits: Ref, ghost: Ref, readsGhost: Ref) returns (res: Bool) requires Lock(bits) ensures Lock(bits) && (res ==> exclusiveResource) { var valRead : Int // valRead := CAS(bits,0,1)_relacq CAS(bits,0,1,valRead,true,true) // return (valRead == 0) res := (valRead == 0) } method lock(bits: Ref, ghost: Ref, readsGhost: Ref) requires Lock(bits) ensures Lock(bits) && exclusiveResource { var count : Int := 0; var outcome : Bool // outcome := try_lock(bits); outcome := try_lock(bits, ghost, readsGhost); while(!outcome) invariant Lock(bits) && (outcome ==> exclusiveResource) { count := count + 1; if(count > 1000) { // sched_yield(); - modelled as skip } // outcome := try_lock(bits); outcome := try_lock(bits, ghost, readsGhost) } } method unlock(bits: Ref, ghost: Ref, readsGhost: Ref) requires Lock(bits) && exclusiveResource ensures Lock(bits) { var tmpInt : Int// dummy variable only needed because our fetch-update macro always returns a value // fetch-and-bitwise-and(bits,~(0x3))__relacq // (was rel in original code) fetchUpdate(bits,tmpInt,zeroFirstBit(zeroSecondBit(tmpInt)),true, true) } // This code is not the original, but is an alternative implementation which avoids incrementing the integer unless there are only readers. This makes the reasoning // something that can be captured by RSL invariants, but is a less efficient implementation (both due to interference from other readers, and due to a CAS rather than fetchUpdate) method try_lock_shared_stronger(bits: Ref, ghost: Ref, readsGhost: Ref) returns (res: Bool) requires Lock(bits) ensures Lock(bits) && (res ==> readResource) { var value : Int var newValue : Int while(true) invariant Lock(bits) { // value := [bits]_rlx; // see if we can read a value which suggests we could get the lock atomicRead(bits,value,false) if(firstBit(value) == 1 || secondBit(value) == 1) { // return false; // the lock is taken res := false goto return } // try to CAS from the earlier-read value; could fail due to other accesses // newValue := CAS(bits,value,value+4)_relacq // (was acq in original code) CAS(bits,value,value + 4,newValue,true,true) // we increment by 4 only if there are only readers if(newValue == value) { // return true; res := true goto return } } label return } method lock_shared(bits: Ref, ghost:Ref, readsGhost:Ref) requires Lock(bits) ensures Lock(bits) && readResource { var count : Int := 0 var success : Bool := false while(!success) invariant Lock(bits) && (success ==> readResource) { success := try_lock_shared_stronger(bits, ghost, readsGhost) } } method unlock_shared(bits: Ref, ghost:Ref, readsGhost:Ref) requires Lock(bits) && readResource ensures Lock(bits) { var tmpValue : Int // fetch-and-increment(bits,-4)__relacq // (was rel in original code) fetchUpdate(bits,tmpValue,tmpValue - 4,true,true) } // This is a reimplementation; the code in // FollyRWSpinlock.vpr is the original. Rather than first "reserving" the // shared lock, and then releasing the write lock, both are // performed by the latter fetch-update simultaneously. // This could be argued to be an optimisation of the original code. method unlock_and_lock_shared_stronger(bits:Ref, ghost:Ref, readsGhost:Ref) requires Lock(bits) && exclusiveResource ensures Lock(bits) && readResource { var tmpValue : Int// dummy variable only needed because our fetch-update macro always returns a value // deal with upgradeable bit (only important for upgradeable mode of the lock) // fetch-and-bitwise-and(bits,~(0x2))_relacq // (was rlx in original code) fetchUpdate(bits,tmpValue,setSecondBit(tmpValue,0),true,true) // fetch-and-increment(bits,3)_relacq // (was rel in original code) fetchUpdate(bits,tmpValue,tmpValue + 3,true,true) //assert tmpValue % 2 == 1 // NOTE: this is an optimisation of the original code! We can prove from the invariant that we must be downgrading the exclusive lock } // PART 2: invariant definitions + example-specific background definitions predicate resource(l : Ref) // represents data protected by lock // Q0 := (v < 0 ? false : ghostRef(ghost) && acc(ghost, leftover(v)) && realRef(bits) && acc(resource(bits), leftover(v)) && ghostRef(readsGhost) && acc(readsGhost, write - rd * (v/4))) // (see below for further definitions) define INV0MaybeUp(v,sync) (v < 0 ? false : ghostRef(ghost) && acc(maybeUp(ghost,!sync).val, leftover(v)) && realRef(bits) && acc(resource(maybeUp(bits,!sync)), leftover(v)) && ghostRef(readsGhost) && acc(maybeUp(readsGhost,!sync).val, write - rds(divide(v,4)))) define INV0MaybeDown(v,sync) (v < 0 ? false : ghostRef(ghost) && acc(maybeDown(ghost,!sync).val, leftover(v)) && realRef(bits) && acc(resource(maybeDown(bits,!sync)), leftover(v)) && ghostRef(readsGhost) && acc(maybeDown(readsGhost,!sync).val, write - rds(divide(v,4)))) define INV0TempOrMaybeUp(v,sync) (v < 0 ? false : ghostRef(ghost) && acc(maybeUp(ghost,!sync).val, leftover(v) - min(leftover(v),perm(temp(ghost).val))) && acc(temp(ghost).val, min(leftover(v),perm(temp(ghost).val))) && realRef(bits) && acc(resource(maybeUp(bits,!sync)), leftover(v) - min(leftover(v),perm(resource(temp(bits))))) && acc(resource(temp(bits)), min(leftover(v),perm(resource(temp(bits))))) && ghostRef(readsGhost) && acc(maybeUp(readsGhost,!sync).val, write - rds(divide(v,4)) - min(write - rds(divide(v,4)), perm(temp(readsGhost).val)))) && acc(temp(readsGhost).val, min(write - rds(divide(v,4)), perm(temp(readsGhost).val))) define INV0Temp(v) (v < 0 ? false : ghostRef(ghost) && acc(temp(ghost).val, leftover(v)) && realRef(bits) && acc(resource(temp(bits)), leftover(v)) && ghostRef(readsGhost) && acc(temp(readsGhost).val, write - rds(divide(v,4)))) // leftover(v) (v % 2 == 1 ? 0 : (secondBit(v) == 1 ? upgradeable - rd * (v/4) : 1 - rd * (v/4)))) // permissions conceptually "left" in the atomic location's invariant define leftover(v) (v % 2 == 1 ? none : (secondBit(v) == 1 ? upgradeable - rds(divide(v,4)) : write - rds(divide(v,4)))) // Define lock concepts: what it means to know a reference is a "Lock", when exclusive, upgradeable and read access to the lock are represented by // Lock(bits) := Rel(bits,Q0) && RMWAcq(bits,Q0) && Init(bits) && realRef(bits) define Lock(bits) realRef(bits) && Rel(bits,0) && RMWAcq(bits,0) && Init(bits) // "write" is a full permission define upgradeable (write*2)/3 // amount of permission representing an upgradeable lock - note: other values e.g. write/3 also work // read permission to each of: the resource guarded by the lock, and the two ghost locations define readResource realRef(bits) && acc(resource(bits),rd()) && ghostRef(ghost) && acc(ghost.val,rd()) && ghostRef(readsGhost) && acc(readsGhost.val,rd()) // full permission to the resource, and the "ghost" ghost reference. define exclusiveResource realRef(bits) && acc(resource(bits),write) && ghostRef(ghost) && acc(ghost.val,write) // counting permissions domain reads { function rd() : Perm function rds(i: Int) : Perm // Note: this axiom allows constraining a "rd" amount to be arbitrarily small, depending on the terms used to instantiate the axiom. // (terms of the form rds(i) will cause an instantiation). The axiom in the current form depends on this triggering for soundness. // In particular, instantiating the axiom with an expression in terms of rd() itself (such as 1/ rd + 1) would lead to unsoundness. However, // we only instantiate the axiom with integer values from the program, which are never expressed in terms of "rd". // An alternative formulation which would not depend on triggering for soundness, would be to make the notion of a machine integer value // an explicit concept in the axiomatisation, and to guard the axiom body with the condition that i is such an integer; this could be done routinely, // but the extra clutter involved would be better generated by a front-end, rather than encoded by hand, as for these examples. axiom bounds { forall i : Int :: {rds(i)} rds(0) == none && (i >= 0 ==> rds(i) < upgradeable) } axiom rdPositive { rd() > none } axiom addition {forall i:Int, j:Int :: {rds(i),rds(j)} i+1 == j ==> rds(i) + rd() == rds(j) } } define divide(a,b) a/b //define divide(a,b) (a - (a % b))/b // this works better than Z3's native division, when dealing with non-linear arithmetic // Viper does not support bit-wise operations - add them here define firstBit(v) v % 2 define secondBit(v) divide(v % 4, 2) function zeroFirstBit(v:Int) : Int // set first bit of v to 0 // requires v >= 0 { (v % 2 == 0 ? v : v - 1) } function zeroSecondBit(v: Int) : Int // set second bit of v to 0 // requires v >= 0 { (v % 4 == 0 || v % 4 == 1) ? v : v - 2 } function setFirstBit(v: Int, b: Int) : Int // set first bit of v to b // requires v >= 0 && (b == 0 || b == 1) { (v % 2 == b ? v : v + (b == 0 ? -1 : 1)) } function setSecondBit(v: Int, b:Int) : Int // set second bit of v to b // requires v >= 0 && (b == 0 || b == 1) { (v % 4 == b * 2 || v % 4 == b * 2 + 1) ? v : v + (b == 0 ? -2 : 2) } define INV1Temp(v) true // not used for this example define INV1TempOrMaybeUp(v,sync) true // not used for this example define INV1MaybeUp(v,sync) true // not used for this example define INV1MaybeDown(v,sync) true // not used for this example define INV1True(v) true // not used for this example define INV2Temp(v) true // not used for this example define INV2TempOrMaybeUp(v,sync) true // not used for this example define INV2MaybeUp(v,sync) true // not used for this example define INV2MaybeDown(v,sync) true // not used for this example define INV2True(v) true // not used for this example // Part 3: standard background definitions (common for all examples) define min(a,b) (a < b ? a : b) method havocedInt() returns (x:Int) method havocedBool() returns (x:Bool) method havocedRefSet() returns (x:Set[Ref]) field val : Int field init: Bool // value is used for nonatomics, only permissions are used for atomics field rel: Int field acq: Bool // use true to indicate RMWAcq, false to indicate normal Acq define realRef(x) !is_ghost(x) && heap(x) == 0 define ghostRef(x) is_ghost(x) && heap(x) == 0 define SomeRel(x) acc(x.rel, wildcard) define SomeAcq(x) acc(x.acq, wildcard) && x.acq == true define SomeRMWAcq(x) acc(x.acq, wildcard) && x.acq == false define SomeAcqOrRMWAcq(x) acc(x.acq, wildcard) // these shorthands work if the parameter to the Acq is representable by a single indexed assertion // (otherwise we have to expand by hand to e.g. SomeAcq(x) && AcqConjunct(x,i1) && AcqConjunct(x,i2) ...) define Acq(x, idx) SomeAcq(x) && AcqConjunct(x, idx) && // here, we take care to (re-)initialise the value of valsRead *only* if we didn't already hold a copy of this conjunct (i.e., we hold exactly one (1/1) now) // A Viper inhale-exhale assertion [A1,A2] has the meaning that A1 is used when inhaling (where the care here must be taken), and A2 when exhaling [perm(AcqConjunct(x, idx)) == 1/1 ==> valsRead(x,idx) == Set[Int](), valsRead(x,idx) == Set[Int]()] define Rel(x, idx) SomeRel(x) && x.rel == idx define RMWAcq(x, idx) SomeRMWAcq(x) && acc(AcqConjunct(x, idx), wildcard) predicate AcqConjunct(x: Ref, idx: Int) function AcqConjunctTrigger(x: Ref, idx: Int) : Bool { true } // used for triggering quantifiers regarding AcqConjunct predicates (since Viper doesn't support predicate instances as triggers, directly) function valsRead(x: Ref, index:Int) : Set[Int] requires AcqConjunct(x,index) define hasAcqConjunct(x,idx,isRMW) (isRMW ? perm(AcqConjunct(x,idx)) > none : perm(AcqConjunct(x,idx)) >= write) && AcqConjunctTrigger(x,idx) define Init(x) acc(x.init, wildcard) define Uninit(x) acc(x.init) && acc(x.val) && !x.init define PointsTo(x,v) acc(x.init) && acc(x.val) && x.init && x.val == v domain parallelHeaps { function up(x: Ref) : Ref function down(x: Ref) : Ref function up_inv(x: Ref) : Ref function down_inv(x: Ref) : Ref function temp(x: Ref) : Ref function temp_inv(x: Ref) : Ref function heap(x: Ref) : Int function is_ghost(x:Ref) : Bool axiom inv_up { forall r:Ref :: {up(r)} up_inv(up(r)) == r && (is_ghost(r) ? up(r) == r : heap(r)==0 ==> heap(up(r)) == 1) } axiom inv_up_inv { forall r:Ref :: {up_inv(r)} up(up_inv(r)) == r && (is_ghost(r) ? up_inv(r) == r : heap(r)==1 ==> heap(up_inv(r)) == 0) } axiom inv_down { forall r:Ref :: {down(r)} down_inv(down(r)) == r && (is_ghost(r) ? down(r) == r : heap(r)==0 ==> heap(down(r)) == -1) } axiom inv_down_inv { forall r:Ref :: {down_inv(r)} down(down_inv(r)) == r && (is_ghost(r) ? down_inv(r) == r : heap(r)==-1 ==> heap(down_inv(r)) == 0) } axiom inv_temp { forall r:Ref :: {temp(r)} temp_inv(temp(r)) == r && (is_ghost(r) ? temp(r) == r : heap(r)==0 ==> heap(temp(r)) == -3) } axiom inv_temp_inv { forall r:Ref :: {temp_inv(r)} temp(temp_inv(r)) == r && (is_ghost(r) ? temp_inv(r) == r : heap(r)==-3 ==> heap(temp_inv(r)) == 0) } } define allocAtomic(x, idx, isRMW) { x := new() assume realRef(x) inhale SomeRel(x) && x.rel == idx && (isRMW ? SomeRMWAcq(x) && acc(AcqConjunct(x,idx),wildcard) : SomeAcq(x) && AcqConjunct(x,idx) && valsRead(x,idx) == Set[Int]()) } define relaxedWrite(x,v) { atomicWrite(x,v,false) } define releaseWrite(x,v) { atomicWrite(x,v,true) } define atomicWrite(x, v, sync) { assert SomeRel(x) atomicWriteExhale(x, v, sync) inhale Init(x) } define waitOnRelaxedRead(x,v) { waitOnAtomicRead(x,v,false) } define waitOnAcquireRead(x,v) { waitOnAtomicRead(x,v,true) } define waitOnAtomicRead(x,v,sync) { var tmp: Int // used as temporary variable for atomic reads var intSet : Set[Int] waitOnAtomicReadWithVars(x,v,sync,tmp,intSet) } define waitOnAtomicReadWithVars(x,v,sync,tmpInt,tmpIntSet) { atomicReadWithVar(x,tmpInt,sync,tmpIntSet) if(tmpInt == v) { // all *subsequent* reads of the same value v will not change anything - only the *last* read (which breaks out of the loop) makes a change to what we hold (and the invariant) atomicReadWithVar(x,tmpInt,sync,tmpIntSet) // assign the *last* value read assume tmpInt != v } } define waitOnCAS(x,v1,v2, readSync, writeSync) { var tmpInt : Int waitOnCASWithVars(x,v1,v2, readSync, writeSync, tmpInt) } define waitOnCASWithVars(x,v1,v2, readSync, writeSync, tmpInt) { // all failing CAS operations will not affect what we hold; they can be skipped, here! CAS(x, v1, v2, tmpInt, readSync, writeSync) // model the *last* CAS, which succeeds, breaking out of the loop assume tmpInt == v1 // the last CAS succeeds } define atomicRead(x, tmp, sync) { var tmpSetAtomicRead : Set[Int] atomicReadWithVar(x, tmp, sync, tmpSetAtomicRead) } define atomicReadWithVar(x, tmp, sync, tmpSet) { assert Init(x) && SomeAcqOrRMWAcq(x) tmp := havocedInt() if(x.acq) { // we have the usual Acq permission atomicReadInhaleWithVar(x, tmp, sync, false, tmpSet) } //else { // attempting atomic read with only RMWAcq permission // CASFailedRead(x,tmp) //} } define relaxedRead(x, tmp) { var tmpSet : Set[Int] relaxedReadWithVar(x, tmp, tmpSet) } define relaxedReadWithVar(x, tmp, tmpSet) { atomicReadWithVar(x, tmp, false, tmpSet) } // Could add macro for general loops define allocNonAtomic(x) { x := new() assume realRef(x) inhale Uninit(x) } define allocGhost(x) { x := new() assume ghostRef(x) inhale Uninit(x) } define CAS(x, v1, v2, tmp, readSync, writeSync) { var tmpIntSet : Set[Int] var tmpRefSet : Set[Ref] CASWithVar(x, v1, v2, tmp, readSync, writeSync, tmpIntSet, tmpRefSet) } define CASWithVar(x, v1, v2, tmp, readSync, writeSync, tmpIntSet, tmpRefSet) { CASGeneralised(x, tmp, tmp==v1, v2, readSync, writeSync, tmpIntSet, tmpRefSet) } define CASGeneralised(x, tmp, condition, newVal, readSync, writeSync, tmpIntSet, tmpRefSet) { assert Init(x) && SomeRMWAcq(x) tmp := havocedInt() if(condition) { if(readSync && writeSync) { // can use RSL rule atomicReadInhaleWithVar(x, tmp, readSync, true, tmpIntSet) atomicWrite(x, newVal, writeSync) } else { CASReadInhaleToTempHeapWithVar(x,tmp,tmpIntSet) atomicWriteExhaleGeneralised(x, newVal, writeSync, true) moveTempHeap(tmpRefSet,readSync) } } //else { //CASFailedRead(x,tmp) //} } define fetchUpdate(x, tmp, newVal, readSync, writeSync) { var tmpIntSet : Set[Int] var tmpRefSet : Set[Ref] fetchUpdateWithVar(x, tmp, newVal, readSync, writeSync, tmpIntSet, tmpRefSet) } // we model a fetchUpdate as a CAS which can never fail (there is no condition on the value read) define fetchUpdateWithVar(x, tmp, newVal, readSync, writeSync, tmpIntSet, tmpRefSet) { CASGeneralised(x, tmp, true, newVal, readSync, writeSync, tmpIntSet, tmpRefSet) } // note: this macro always picks the same variable names, so doesn't work multiple times in the same scope (since we don't have local variable scopes). Use the macro below if this is problematic (and declare the variables outside) define FENCEAcq() { var refSet : Set[Ref] FENCEAcqWithVars(refSet) } define maybeDown(x, goDown) (goDown ? down(x) : x) define maybeUp(x, goUp) (goUp ? up(x) : x) define atomicWriteExhale(x, v, sync) { atomicWriteExhaleGeneralised(x,v,sync,false) } define rewriteAcqConjuncts(x,isRMW,oldAcqSet,newAcqSet) { var tmpBool : Bool var tmpInt : Int rewriteAcqConjunctsWithVar(x,isRMW,oldAcqSet,newAcqSet,tmpBool,tmpInt) } // The following definitions need to be expanded to cover at least enough indices for the invariant numbering (but are otherwise independent of the example): define FENCEAcqWithVars(refSet) { // move all locations r to which permission to "init" is held from "down" heap to normal heap refSet := havocedRefSet() assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(down(r).init) > none assume forall r: Ref :: {down(r).init} perm(down(r).init) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(r.init, perm(down(r).init)) assume forall r: Ref :: {r in refSet}{down(r)} r in refSet ==> r.init == down(r).init exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(down(r).init, perm(down(r).init)) refSet := havocedRefSet() // move all locations r to which permission to "vals" is held from "down" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(down(r).val) > none assume forall r: Ref :: {down(r).val} perm(down(r).val) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(r.val, perm(down(r).val)) assume forall r: Ref :: {r in refSet}{down(r)} r in refSet ==> r.val == down(r).val exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(down(r).val, perm(down(r).val)) refSet := havocedRefSet() // move all locations r to which permission to "rel" is held from "down" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(down(r).rel) > none assume forall r: Ref :: {down(r).rel} perm(down(r).rel) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(r.rel, perm(down(r).rel)) assume forall r: Ref :: {r in refSet}{down(r)} r in refSet ==> r.rel == down(r).rel exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(down(r).rel, perm(down(r).rel)) refSet := havocedRefSet() // move all locations r to which permission to "acq" is held from "down" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(down(r).acq) > none assume forall r: Ref :: {down(r).acq} perm(down(r).acq) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(r.acq, perm(down(r).acq)) assume forall r: Ref :: {r in refSet}{down(r)} r in refSet ==> r.acq == down(r).acq exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(down(r).acq, perm(down(r).acq)) // UNROLL per indexed invariant (0,1, ...) and for both RelDisjunct and AcqConjunct... refSet := havocedRefSet() // move all locations r to which permission to "AcqConjunct(r,0)" is held from "down" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(AcqConjunct(down(r),0)) > none assume forall r: Ref :: {down(r)} perm(AcqConjunct(down(r),0)) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> acc(AcqConjunct(r,0), perm(AcqConjunct(down(r),0))) assume forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> valsRead(r,0) == valsRead(down(r),0) exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(AcqConjunct(down(r),0), perm(AcqConjunct(down(r),0))) refSet := havocedRefSet() // move all locations r to which permission to "AcqConjunct(r,1)" is held from "down" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(AcqConjunct(down(r),1)) > none assume forall r: Ref :: {down(r)} perm(AcqConjunct(down(r),1)) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> acc(AcqConjunct(r,1), perm(AcqConjunct(down(r),1))) assume forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> valsRead(r,1) == valsRead(down(r),1) exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(AcqConjunct(down(r),1), perm(AcqConjunct(down(r),1))) refSet := havocedRefSet() // move all locations r to which permission to "AcqConjunct(r,2)" is held from "down" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(AcqConjunct(down(r),2)) > none assume forall r: Ref :: {down(r)} perm(AcqConjunct(down(r),2)) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> acc(AcqConjunct(r,2), perm(AcqConjunct(down(r),2))) assume forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> valsRead(r,2) == valsRead(down(r),2) exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(AcqConjunct(down(r),2), perm(AcqConjunct(down(r),2))) refSet := havocedRefSet() // move all locations r to which permission to "resource(r)" is held from "down" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(resource(down(r))) > none assume forall r: Ref :: {down(r)} perm(resource(down(r))) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> acc(resource(r), perm(resource(down(r)))) exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(resource(down(r)), perm(resource(down(r)))) } define moveTempHeap(refSet, readSync) { // move all locations r to which permission to "init" is held from "temp" heap to normal heap refSet := havocedRefSet() assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(temp(r).init) > none assume forall r: Ref :: {temp(r).init} perm(temp(r).init) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(maybeDown(r,!readSync).init, perm(temp(r).init)) assume forall r: Ref :: {r in refSet}{temp(r)} r in refSet ==> maybeDown(r,!readSync).init == temp(r).init exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(temp(r).init, perm(temp(r).init)) refSet := havocedRefSet() // move all locations r to which permission to "vals" is held from "temp" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(temp(r).val) > none assume forall r: Ref :: {temp(r)} perm(temp(r).val) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(maybeDown(r,!readSync).val, perm(temp(r).val)) assume forall r: Ref :: {r in refSet}{temp(r)} r in refSet ==> maybeDown(r,!readSync).val == temp(r).val exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(temp(r).val, perm(temp(r).val)) refSet := havocedRefSet() // move all locations r to which permission to "rel" is held from "temp" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(temp(r).rel) > none assume forall r: Ref :: {temp(r).rel} perm(temp(r).rel) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(maybeDown(r,!readSync).rel, perm(temp(r).rel)) assume forall r: Ref :: {r in refSet}{temp(r)} r in refSet ==> maybeDown(r,!readSync).rel == temp(r).rel exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(temp(r).rel, perm(temp(r).rel)) refSet := havocedRefSet() // move all locations r to which permission to "acq" is held from "temp" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(temp(r).acq) > none assume forall r: Ref :: {temp(r).acq} perm(temp(r).acq) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(maybeDown(r,!readSync).acq, perm(temp(r).acq)) assume forall r: Ref :: {r in refSet}{temp(r)} r in refSet ==> maybeDown(r,!readSync).acq == temp(r).acq exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(temp(r).acq, perm(temp(r).acq)) // UNROLL per indexed invariant (0,1, ...) for AcqConjunct... refSet := havocedRefSet() // move all locations r to which permission to "AcqConjunct(r,0)" is held from "temp" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(AcqConjunct(temp(r),0)) > none assume forall r: Ref :: {temp(r)} perm(AcqConjunct(temp(r),0)) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(AcqConjunct(maybeDown(r,!readSync),0), perm(AcqConjunct(temp(r),0))) assume forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> valsRead(maybeDown(r,!readSync),0) == valsRead(temp(r),0) exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(AcqConjunct(temp(r),0), perm(AcqConjunct(temp(r),0))) refSet := havocedRefSet() // move all locations r to which permission to "AcqConjunct(r,1)" is held from "temp" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(AcqConjunct(temp(r),1)) > none assume forall r: Ref :: {temp(r)} perm(AcqConjunct(temp(r),1)) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(AcqConjunct(maybeDown(r,!readSync),1), perm(AcqConjunct(temp(r),1))) assume forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> valsRead(maybeDown(r,!readSync),1) == valsRead(temp(r),1) exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(AcqConjunct(temp(r),1), perm(AcqConjunct(temp(r),1))) refSet := havocedRefSet() // move all locations r to which permission to "AcqConjunct(r,2)" is held from "temp" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(AcqConjunct(temp(r),2)) > none assume forall r: Ref :: {temp(r)} perm(AcqConjunct(temp(r),2)) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(AcqConjunct(maybeDown(r,!readSync),2), perm(AcqConjunct(temp(r),2))) assume forall r: Ref :: {r in refSet} {down(r)} r in refSet ==> valsRead(maybeDown(r,!readSync),2) == valsRead(temp(r),2) refSet := havocedRefSet() // move all locations r to which permission to "resource(r)" is held from "temp" heap to normal heap assume forall r: Ref :: {r in refSet} r in refSet ==> heap(r) == 0 && !is_ghost(r) && perm(resource(temp(r))) > none assume forall r: Ref :: {temp(r)} perm(resource(temp(r))) > none && !is_ghost(r) ==> r in refSet inhale forall r: Ref :: {r in refSet} r in refSet ==> acc(resource(maybeDown(r,!readSync)), perm(resource(temp(r)))) exhale forall r: Ref :: {r in refSet} r in refSet ==> acc(resource(temp(r)), perm(resource(temp(r)))) } define rewriteAcqConjunctsWithVar(x,isRMW,oldAcqSet,newAcqSet,tmpBool,tmpInt) { assert SomeAcq(x) tmpBool := havocedBool() if(tmpBool) { // check rewriting is justified // remove all permissions from current state exhale forall r: Ref :: r != null ==> acc(r.init, perm(r.init)) exhale forall r: Ref :: r != null ==> acc(r.val, perm(r.val)) exhale forall r: Ref :: r != null ==> acc(r.rel, perm(r.rel)) exhale forall r: Ref :: r != null ==> acc(r.acq, perm(r.acq)) //exhale forall r: Ref :: r != null ==> acc(AcqConjunct(r,0), (perm(AcqConjunct(r,0)) > none ? perm(AcqConjunct(r,0)) : none)) //exhale forall r: Ref :: r != null ==> acc(AcqConjunct(r,1), perm(AcqConjunct(r,1))) //exhale forall r: Ref :: r != null ==> acc(AcqConjunct(r,2), perm(AcqConjunct(r,2))) tmpInt := havocedInt() // UNROLL per numbered invariant if(0 in oldAcqSet) { inhale INV0MaybeDown(tmpInt,true) } if(1 in oldAcqSet) { inhale INV1MaybeDown(tmpInt,true) } if(2 in oldAcqSet) { inhale INV2MaybeDown(tmpInt,true) } // UNROLL per numbered invariant if(0 in newAcqSet) { exhale INV0MaybeDown(tmpInt,true) } if(1 in newAcqSet) { exhale INV1MaybeDown(tmpInt,true) } if(2 in newAcqSet) { exhale INV2MaybeDown(tmpInt,true) } assume false // kill this branch - we've generated sufficient checks to ensure that the rewriting is OK } if(isRMW) { exhale forall i:Int :: i in oldAcqSet ==> acc(AcqConjunct(x,i),perm(AcqConjunct(x,i))) inhale forall i:Int :: i in newAcqSet ==> acc(AcqConjunct(x,i),wildcard) } else { exhale forall i:Int :: i in oldAcqSet ==> AcqConjunct(x,i) && valsRead(x,i) == Set[Int]() inhale forall i:Int :: i in newAcqSet ==> AcqConjunct(x,i) && valsRead(x,i) == Set[Int]() } } // These definitions need to be expanded to cover at least enough indices for the invariant numbering (but are otherwise independent of the example): define allocAtomicIndexSet(x, RelInv, AcqInvSet, isRMW) { x := new() assume realRef(x) inhale Rel(x, RelInv) && (isRMW ? SomeRMWAcq(x) : SomeAcq(x)) // UNROLL per numbered invariant if (0 in AcqInvSet) { inhale isRMW ? acc(AcqConjunct(x,0),wildcard) : AcqConjunct(x,0) && valsRead(x,0) == Set[Int]() } if (1 in AcqInvSet) { inhale isRMW ? acc(AcqConjunct(x,1),wildcard) : AcqConjunct(x,1) && valsRead(x,1) == Set[Int]() } if (2 in AcqInvSet) { inhale isRMW ? acc(AcqConjunct(x,2),wildcard) : AcqConjunct(x,2) && valsRead(x,2) == Set[Int]() } } define atomicWriteExhaleGeneralised(x, v, sync, useTempHeap) { // UNROLL per numbered invariant if(x.rel == 0) { if(useTempHeap) { exhale INV0TempOrMaybeUp(v,sync) } else { exhale INV0MaybeUp(v,sync) } } elseif(x.rel == 1) { if(useTempHeap) { exhale INV1TempOrMaybeUp(v,sync) } else { exhale INV1MaybeUp(v,sync) } } elseif(x.rel == 2) { if(useTempHeap) { exhale INV2TempOrMaybeUp(v,sync) } else { exhale INV2MaybeUp(v,sync) } } else { assert false // this cannot happen - no Rel invariant was held! } } define atomicReadInhaleWithVar(x, v, sync, isRMW, tmpSet) { // UNROLL per numbered invariant if(hasAcqConjunct(x,0,isRMW) && (isRMW || !(v in valsRead(x,0)))) { if(!isRMW) { tmpSet := valsRead(x,0) exhale AcqConjunct(x,0) assert perm(AcqConjunct(x,0)) == none // we don't support multiple copies of same AcqConjunct, yet inhale AcqConjunct(x,0) && valsRead(x,0) == tmpSet union Set(v) } inhale INV0MaybeDown(v,sync) } if(hasAcqConjunct(x,1,isRMW) && (isRMW || !(v in valsRead(x,1)))) { if(!isRMW) { tmpSet := valsRead(x,1) exhale AcqConjunct(x,1) assert perm(AcqConjunct(x,1)) == none // we don't support multiple copies of same AcqConjunct, yet inhale AcqConjunct(x,1) && valsRead(x,1) == tmpSet union Set(v) } inhale INV1MaybeDown(v,sync) } if(hasAcqConjunct(x,2,isRMW) && (isRMW || !(v in valsRead(x,2)))) { if(!isRMW) { tmpSet := valsRead(x,2) exhale AcqConjunct(x,2) assert perm(AcqConjunct(x,2)) == none // we don't support multiple copies of same AcqConjunct, yet inhale AcqConjunct(x,2) && valsRead(x,2) == tmpSet union Set(v) } inhale INV2MaybeDown(v,sync) } } define CASReadInhaleToTempHeapWithVar(x,v,tmpSet) { // UNROLL per numbered invariant if(hasAcqConjunct(x,0,true)) { inhale INV0Temp(v) } if(hasAcqConjunct(x,1,true)) { inhale INV1Temp(v) } if(hasAcqConjunct(x,2,true)) { inhale INV2Temp(v) } }