# Specification

So far, we have used Harmony to implement various algorithms. But Harmony can also be used to specify what an algorithm is supposed to do. For example, Figure 8.1 specifies the intended behavior of a lock. In this case, a lock is a boolean, initially False, with two operations, acquire() and release(). The acquire() operation waits until the lock is False and then sets it to True in an atomic operation. The release() operation sets the lock back to False. The code is similar to Figure 5.3, except that waiting for the lock to become available and taking it is executed as an atomic operation.

synch.hny
import list
import bag

def tas(lk):
atomically:
result = !lk
!lk = True

def cas(p, old, new):
atomically:
result = !p == old
if result:
!p = new

def BinSema(acquired):
result = acquired

def Lock():
result = BinSema(False)

def acquired(binsema):
result = !binsema

def acquire(binsema):
atomically when not !binsema:
!binsema = True

def release(binsema):
assert !binsema
atomically !binsema = False

def held(binsema):
result = !binsema

def Condition():
result = bag.empty()

def wait(c, lk):
var cnt = 0
let (), ctx = save():
atomically:
cnt = bag.multiplicity(!c, ctx)
!c = bag.add(!c, ctx)
!lk = False
atomically when (not !lk) and (bag.multiplicity(!c, ctx) <= cnt):
!lk = True

def notify(c):
atomically if !c != bag.empty():
!c = bag.remove(!c, bag.bchoose(!c))

def notifyAll(c):
atomically !c = bag.empty()

def Semaphore(cnt):
result = cnt

def P(sema):
atomically when !sema > 0:
!sema -= 1

def V(sema):
atomically !sema += 1

def Queue():
result = []

def get(q):
atomically when !q != []:
!q = list.tail(!q)

def put(q, item):
atomically !q = list.append(!q, item)
cssynch.hny
import synch

const NTHREADS = 2

lock = synch.Lock()

while choose({ False, True }):
synch.acquire(?lock)
cs: assert countLabel(cs) == 1
synch.release(?lock)

for i in {1..NTHREADS}:
UpLock.hny
from synch import Lock, acquire, release

sequential done

count = 0
countlock = Lock()
done = [ False, False ]

acquire(?countlock)
count = count + 1
release(?countlock)
done[self] = True
await done[1 - self]
assert count == 2