diff --git a/code/2pc1.hny b/code/2pc1.hny deleted file mode 100644 index 0542e8b3..00000000 --- a/code/2pc1.hny +++ /dev/null @@ -1,31 +0,0 @@ -network = {} - -def send(msg): - atomically network |= { msg } - -def bank(self, _balance): - var balance = _balance - var status, received = (), {} - while True: - atomically when exists req in network - received when req.dst == self: - received |= { req } - if req.request == "withdraw": - if (status != ()) or (req.amount > balance): - send({ .dst: req.src, .src: self, .response: "no" }) - else: - status = balance - balance -= req.amount - send({ .dst: req.src, .src: self, .response: "yes", .funds: balance }) - elif req.request == "deposit": - if status != (): - send({ .dst: req.src, .src: self, .response: "no" }) - else: - status = balance - balance += req.amount - send({ .dst: req.src, .src: self, .response: "yes", .funds: balance }) - elif req.request == "commit": - assert status != () - status = () - else: - assert (status != ()) and (req.request == "abort") - balance, status = status, () diff --git a/code/2pc2.hny b/code/2pc2.hny deleted file mode 100644 index 9aa730c7..00000000 --- a/code/2pc2.hny +++ /dev/null @@ -1,35 +0,0 @@ -import list - -def transfer(self, b1, b2, amt): - send({ .dst: b1, .src: self, .request: "withdraw", .amount: amt }) - send({ .dst: b2, .src: self, .request: "deposit", .amount: amt }) - atomically let msgs = { m for m in network where m.dst == self } - when { m.src for m in msgs } == { b1, b2 }: - if all(m.response == "yes" for m in msgs): - for m in msgs where m.response == "yes": - send({ .dst: m.src, .src: self, .request: "commit" }) - else: - for m in msgs where m.response == "yes": - send({ .dst: m.src, .src: self, .request: "abort" }) - -def check(self, total): - let allbanks = { (.bank, i) for i in { 1 .. NBANKS } }: - for bank in allbanks: - send({ .dst: bank, .src: self, .request: "withdraw", .amount: 0 }) - atomically let msgs = { m for m in network where m.dst == self } - when { m.src for m in msgs } == allbanks: - assert all(m.response == "yes" for m in msgs) => - (list.sum(m.funds for m in msgs) == total) - for m in msgs where m.response == "yes": - send({ .dst: m.src, .src: self, .request: "abort" }) - -let balances = { i:choose({ 0 .. MAX_BALANCE }) for i in { 1 .. NBANKS } }: - for i in { 1 .. NBANKS }: - spawn eternal bank((.bank, i), balances[i]) - for i in { 1 .. NCOORDS }: - if choose({ "transfer", "check" }) == .transfer: - let b1 = choose({ (.bank, j) for j in { 1 .. NBANKS }}) - let b2 = choose({ (.bank, j) for j in { 1 .. NBANKS }} - { b1 }): - spawn transfer((.coord, i), b1, b2, 1) - else: - spawn check((.coord, i), list.sum(balances)) diff --git a/code/BBsema.hny b/code/BBsema.hny deleted file mode 100644 index 4490c5f2..00000000 --- a/code/BBsema.hny +++ /dev/null @@ -1,27 +0,0 @@ -import synch; - -const NSLOTS = 2; # size of bounded buffer - -def produce(item): - P(?n_empty); - P(?l_in); - buf[b_in] = item; - b_in = (b_in % NSLOTS) + 1; - V(?l_in); - V(?n_full); -; -def consume(): - P(?n_full); - P(?l_out); - result = buf[b_out]; - b_out = (b_out % NSLOTS) + 1; - V(?l_out); - V(?n_empty); -; -buf = { x:() for x in {1..NSLOTS} }; -b_in = 1; -b_out = 1; -l_in = Semaphore(1); -l_out = Semaphore(1); -n_full = Semaphore(0); -n_empty = Semaphore(NSLOTS); diff --git a/code/BBsematest.hny b/code/BBsematest.hny deleted file mode 100644 index 24c02ade..00000000 --- a/code/BBsematest.hny +++ /dev/null @@ -1,11 +0,0 @@ -import BBsema; - -const NPRODS = 3; # number of producers -const NCONSS = 3; # number of consumers - -for i in {1..NPRODS}: - spawn produce(i); -; -for i in {1..NCONSS}: - spawn consume(); -; diff --git a/code/DinersCV.hny b/code/DinersCV.hny index 7d52d717..7e5fa2e3 100644 --- a/code/DinersCV.hny +++ b/code/DinersCV.hny @@ -21,7 +21,7 @@ def diner(which): # dine synch.acquire(?mutex) forks[left] = forks[right] = False - synch.notify(?conds[left]); + synch.notify(?conds[left]) synch.notify(?conds[right]) synch.release(?mutex) # think diff --git a/code/RWhoare.hny b/code/RWhoare.hny deleted file mode 100644 index 1b2e17f3..00000000 --- a/code/RWhoare.hny +++ /dev/null @@ -1,58 +0,0 @@ -from synch import Semaphore, P, V - -def mon_enter(): - P(?mutex) - -def mon_exit(): - V(?mutex) - -def H_Condition(mon): - result = { .lock: mon, .sema: Semaphore(0), .count: 0 } - -def H_wait(cond): - cond->count += 1 - V(cond->lock); P(?cond->sema) - cond->count -= 1 - -def H_has_waiters(cond): - result = cond->count > 0 - -def H_signal(cond): - if cond->count > 0: - V(?cond->sema); P(cond->lock) - -mutex = Semaphore(1) -OKtoread = H_Condition(?mutex) -OKtowrite = H_Condition(?mutex) -r_entered, w_entered = 0, 0 - -def acquire_rlock(): - mon_enter() - if w_entered > 0: - H_wait(?OKtoread) - r_entered += 1 - H_signal(?OKtoread) - mon_exit() - -def release_rlock(): - mon_enter() - r_entered -= 1 - if r_entered == 0: - H_signal(?OKtowrite) - mon_exit() - -def acquire_wlock(): - mon_enter() - if (r_entered + w_entered) > 0: - H_wait(?OKtowrite) - w_entered += 1 - mon_exit() - -def release_wlock(): - mon_enter() - w_entered -= 1 - if H_has_waiters(?OKtoread): - H_signal(?OKtoread) - else: - H_signal(?OKtowrite) - mon_exit() diff --git a/code/RWqueue.hny b/code/RWqueue.hny deleted file mode 100644 index 7ded38fb..00000000 --- a/code/RWqueue.hny +++ /dev/null @@ -1,42 +0,0 @@ -import synch; -import list; - -def V_one(): - if queue == []: - V(?mutex); - else: - let h = head(queue): - if (h[0] == .read) and (w_entered == 0): V(h[1]); - elif (h[0] == .write) and ((r_entered + w_entered) == 0): V(h[1]); - else: V(?mutex); - ; - ; - ; -; -def acquire_rlock(psema): - P(?mutex); - if (w_entered > 0) or (queue != []): - queue = append(queue, (.read, psema)); V(?mutex); - P(psema); queue = tail(queue); - ; - r_entered += 1; - V_one(); -; -def release_rlock(): - P(?mutex); r_entered -= 1; V_one(); -; -def acquire_wlock(psema): - P(?mutex); - if (r_entered + w_entered) > 0: - queue = append(queue, (.write, psema)); V(?mutex); - P(psema); queue = tail(queue); - ; - w_entered = 1; - V_one(); -; -def release_wlock(): - P(?mutex); w_entered = 0; V_one(); -; -mutex = Semaphore(1); -r_entered, w_entered = 0, 0; -queue = []; diff --git a/code/paxos1.hny b/code/paxos1.hny deleted file mode 100644 index b43262fa..00000000 --- a/code/paxos1.hny +++ /dev/null @@ -1,24 +0,0 @@ -import bag - -const F = 1 -const NACCEPTORS = (2 * F) + 1 -const NLEADERS = F + 1 -const NBALLOTS = 2 - -network = bag.empty() - -proposals = [ choose({0, 1}) for i in {0..NLEADERS-1} ] - -def send(msg): - atomically network = bag.add(network, msg) - -def receive(ballot, phase) returns quorum: - let msgs = { e:c for (b,p,t,e):c in network - where (b,p,t) == (ballot, phase, "B") }: - quorum = bag.combinations(msgs, NACCEPTORS - F) - -print proposals -for i in {0..NLEADERS - 1}: - spawn leader(i + 1, proposals[i]) -for i in {1..NACCEPTORS}: - spawn eternal acceptor() diff --git a/code/paxos2.hny b/code/paxos2.hny deleted file mode 100644 index 2682bd48..00000000 --- a/code/paxos2.hny +++ /dev/null @@ -1,28 +0,0 @@ -def leader(self, proposal): - var ballot, estimate = self, proposal - send(ballot, 1, "A", None) - while ballot <= NBALLOTS: - atomically when exists quorum in receive(ballot, 1): - let accepted = { e for e:_ in quorum where e != None }: - if accepted != {}: - _, estimate = max(accepted) - send(ballot, 2, "A", estimate) - atomically when exists quorum in receive(ballot, 2): - if bag.multiplicity(quorum, (ballot, estimate)) == (NACCEPTORS - F): - assert estimate in proposals # validity - print estimate - ballot += NLEADERS - if ballot <= NBALLOTS: - send(ballot, 1, "A", None) - -def acceptor(): - var ballot, last_accepted, received = 0, None, {} - while True: - atomically when exists b,p,e in { (b,p,e) for b,p,t,e:_ in network - where ((b,p) not in received) and (t == "A") }: - received |= { (b, p) } - if b >= ballot: - ballot = b - if p == 2: - last_accepted = (ballot, e) - send(b, p, "B", last_accepted) diff --git a/code/qsort.hny b/code/qsort.hny index 408e4a56..de3655c0 100644 --- a/code/qsort.hny +++ b/code/qsort.hny @@ -2,7 +2,7 @@ def Qsort(arr) returns state: state = { .arr: arr, .todo: { (0, len(arr) - 1) } } def swap(p, q): # swap !p and !q - !p, !q = !q, !p; + !p, !q = !q, !p def partition(qs, lo, hi) returns pivot: pivot = lo @@ -10,7 +10,7 @@ def partition(qs, lo, hi) returns pivot: if qs->arr[i] <= qs->arr[hi]: swap(?qs->arr[pivot], ?qs->arr[i]) pivot += 1 - swap(?qs->arr[pivot], ?qs->arr[hi]); + swap(?qs->arr[pivot], ?qs->arr[hi]) def sortrange(qs, range): let lo, hi = range let pivot = partition(qs, lo, hi): diff --git a/code/qsorttest.hny b/code/qsorttest.hny index 1e7e4960..a7722ba8 100644 --- a/code/qsorttest.hny +++ b/code/qsorttest.hny @@ -6,4 +6,4 @@ a = [ choose({1..NITEMS}) for i in {1..choose({1..NITEMS})} ] testqs = qsort.Qsort(a) sa = qsort.sort(?testqs) assert all(sa[i - 1] <= sa[i] for i in {1..len(sa)-1}) # sorted? -assert bag.fromList(a) == bag.fromList(sa); # is it a permutation? +assert bag.fromList(a) == bag.fromList(sa) # is it a permutation? diff --git a/code/rwlock_cheat.hny b/code/rwlock_cheat.hny index e941d8fd..9a564167 100644 --- a/code/rwlock_cheat.hny +++ b/code/rwlock_cheat.hny @@ -4,13 +4,13 @@ def RWlock() returns lock: lock = synch.Lock() def read_acquire(rw): - synch.acquire(rw); + synch.acquire(rw) def read_release(rw): - synch.release(rw); + synch.release(rw) def write_acquire(rw): - synch.acquire(rw); + synch.acquire(rw) def write_release(rw): - synch.release(rw); + synch.release(rw)