# 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)
!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

lock = synch.Lock()

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


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


The code in Figure 8.1 is similar to the code in Harmony's synch module. (The module generalizes locks to binary semaphores (Chapter 16), but the lock interface is the same.) Figure 8.2 shows how locks may be used to implement a critical section. Figure 8.3 gives an example of how locks may be used to fix the program of Figure 3.2.
In Harmony, any statement can be preceded by the atomically keyword. It means that statement as a whole is to be executed atomically. The atomically keyword can be used to specify the behavior of methods such as acquire and release. But an actual executable program---such as the one in Figure 8.2---should not use the atomically keyword because---on a normal machine---it cannot be directly compiled into machine code. If we want to make the program executable on hardware, we have to show how Lock, acquire, and release are implemented, not just how they are specified. Chapter 9 presents such an implementation.