A Formal Reference for SCOOP - Empirical Software Engineering and Verification - page 113

pass locks : REG → PROC PROC TUPLE [ SET [ PROC ] , SET [ PROC ]] REG
k . pass locks ( p , q , ( l r , l c )) require
k . procs . has ( p ) ∧ k . procs . has ( q )
∀ x ∈ l r : k . procs . has ( x ) ∧∀ x ∈ l c : k . procs . has ( x )
∀ x ∈ l r : k . obtained rq locks ( p ) . flat . has ( x ) ∨ k . retrieved rq locks ( p ) . flat . has ( x )
∀ x ∈ l c : x = k . obtained cs lock ( p ) ∨ k . retrieved cs locks ( p ) . flat . has ( x )
¬ k . locks passed ( p )
axioms
k . pass locks ( p , q , ( l r , l c )) . locks passed ( p )=

true if ¬ l r . is empty ∨¬ l c . is empty
false otherwise
k . pass locks ( p , q , ( l r , l c )) . retrieved rq locks ( q )= k . retrieved rq locks ( q ) . push ( l r )
k . pass locks ( p , q , ( l r , l c )) . retrieved cs locks ( q )= k . retrieved cs locks ( q ) . push ( l c )
⎛
⎝

⎞
⎠

p ∧

k . locks passed ( q ) ∧
k . obtained rq locks ( q ) . flat ⊆ l r ∧
k . retrieved rq locks ( q ) . flat ⊆ l r ∧
k . obtained cs lock ( q ) ∈ l c ∧
k . retrieved cs locks ( q ) . flat ⊆ l c

= q

→¬ k . pass locks ( p , q , ( l r , l c )) . locks passed ( q )

The command revoke locks takes a processor p and a processor q . It reverses the effect
of a lock passing operation from a processor p to q and returns an updated instance of
REG . This is only allowed if processor p passed locks to q in a preceding lock passing
operation. Note that the lock passing operation from p to q potentially marked the locks
of q as not passed. Revoking the locks from q to p requires the reverse action. If p has
retrieved locks in common with the locks of q , even after the retrieved locks from p
have been removed from q ,then q 's locks must be marked as passed because they are
now in possession of p .

revoke locks : REG → PROC PROC REG
k . revoke locks ( p , q ) require
k . procs . has ( p ) ∧ k . procs . has ( q )
¬ k . retrieved rq locks ( q ) . is empty ∧¬ k . retrieved cs locks ( q ) . is empty
k . retrieved rq locks ( q ) . top ⊆ k . obtained rq locks ( p ) . flat ∪ k . retrieved rq locks ( p ) . flat
k . retrieved cs locks ( q ) . top ⊆{ k . obtained cs lock ( p ) }∪ k . retrieved cs locks ( p ) . flat
k . retrieved rq locks ( q ) . top ∪ k . retrieved cs locks ( q ) . top = {} → k . locks passed ( p )
¬ k . locks passed ( q )
axioms
¬ k . revoke locks ( p , q ) . locks passed ( p )
k . revoke locks ( p , q ) . retrieved rq locks ( q )= k . retrieved rq locks ( q ) . pop
k . revoke locks ( p , q ) . retrieved cs locks ( q )= k . retrieved cs locks ( q ) . pop
⎛
⎝

⎞
⎠

p = q ∧
⎛
⎝

⎞
⎠

∃ x ∈ k . retrieved rq locks ( p ) . flat : (

k ) ∨

k . retrieved rq locks ( q ) . pop . flat . has ( x )

. obtained rq locks ( q ) . flat . has ( x

) ∨
∃ x ∈ k . retrieved cs locks ( p ) . flat : (
x = k . obtained cs lock ( q ) ∨
k . retrieved cs locks ( q ) . pop . flat . has ( x )

)

→ k . revoke locks ( p , q ) . locks passed ( q )