Project P120
Leader lease
A lease from a store that A trusts by its own clock while B takes over by the store's: two leaders over every pair of clock drifts, counting from asking or hearing, and the margin that removes them and what it costs.
2 modules · 2 recorded sessionstext-menu UI in the terminalupdated 2026-10-16
Every screen below was recorded under CPython. When this page was built, the EML interpreter replayed each session from the same input and printed the same bytes.
About
A holds a lease from a store, then goes quiet. B takes over when the store's clock says the lease has run out, while A trusts its own clock. When A's lease outlasts the store's in real time, there are two leaders, and neither can tell.
main.eml- the menu, the settings, one lease in real time, two leaders over every pair of drifts, and the margin that removes themlease.eml- when A stops, when the store frees the lease and B starts, the time with two leaders or none, and the smallest margin
How each part works:
- Times are whole milliseconds of real time. A clock that drifts d percent counts 100 + d ms for every 100 real ones. A's request takes A's delay to reach the store, and the answer as long again; B keeps asking and hears after B's delay.
- A counts its lease from when it asks, or from when it hears, and stops when its clock has counted the lease less a margin. As in the corpus case
leader-lease-expiry, neither side is wrong about its own clock. - With a lease of 1000 ms, A 30 ms from the store and B 10 ms: - no drift, A counting from when it asks: no leader for 40 ms; - counting from when it hears: two leaders for 20 ms with no drift at all, since A starts late by its delay back; - A's clock 5% slow: two leaders for 13 ms.
- Every pair of drifts within 5%: two leaders in 23 of the 121 pairs, for up to 60 ms. A slow clock keeps A leading longer, and a fast store frees the lease sooner.
- The margin: each pair alone would need from 0 to 57 ms, and a margin safe for every pair has to cover the worst, A slow and the store fast. 57 ms leaves no leader for up to 194 ms at the other pairs; counting from when A hears needs 114 ms. Within 10%, 145 ms and 199 ms.
What is checked: menu choices 1 to 8; a lease from 100 to 5000 ms, longer than the margin; delays from 0 to 100 ms; drifts from -10 to 10 percent and a bound from 0 to 10; send or receive; a margin below the lease. An empty answer cancels.
Sessions: sessions/basic.in gives: - the settings, one lease, every drift and the margin; - A counting from when it hears: one lease and the margin; - A's clock 5% slow: one lease and every drift, then a margin of 57 ms: every drift and one lease again; - a bound of 10%, and the margin for it.
sessions/bad-input.in gives: - menu choices 0 and x; - the lease: a cancel, 50, 6000 and x, then 1000 with a cancel and 101 for A's delay, then 30 with a cancel and -1 for B's; - clocks: a cancel, 11, -11 and x, then 0 with a cancel, 0 0 with a cancel and 11, and 0 0 5 with a cancel and both; - the margin: a cancel, 1000, -1 and x, then 500, a lease of 400 (not longer than the margin), and a margin of 999, where A's lease is over before it hears.
Built on the verified corpus case leader-lease-expiry (two leaders from a lease both sides believe, and a guard that removes them).
Recorded sessions
What the screen shows while someone uses the program. Each typed line appears after its prompt, the way a terminal shows it.
bad-input
interpreter: byte-equal== Leader lease ==
A holds a lease from a store and then goes quiet; B takes over when the store's clock says the lease has run out, while A trusts its own clock.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 0
Pick a number from 1 to 8.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> x
Pick a number from 1 to 8.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)>
Cancelled.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)> 50
Type a whole number from 100 to 5000.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)> 6000
Type a whole number from 100 to 5000.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)> x
Type a whole number from 100 to 5000.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)> 1000
A's delay to the store (0 to 100 ms)>
Cancelled.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)> 1000
A's delay to the store (0 to 100 ms)> 101
Type a whole number from 0 to 100.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)> 1000
A's delay to the store (0 to 100 ms)> 30
B's delay to the store (0 to 100 ms)>
Cancelled.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)> 1000
A's delay to the store (0 to 100 ms)> 30
B's delay to the store (0 to 100 ms)> -1
Type a whole number from 0 to 100.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)>
Cancelled.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> 11
Type a whole number from -10 to 10.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> -11
Type a whole number from -10 to 10.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> x
Type a whole number from -10 to 10.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> 0
the store's clock drift (-10 to 10 percent)>
Cancelled.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> 0
the store's clock drift (-10 to 10 percent)> 0
drift bound for the tables (0 to 10 percent)>
Cancelled.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> 0
the store's clock drift (-10 to 10 percent)> 0
drift bound for the tables (0 to 10 percent)> 11
Type a whole number from 0 to 10.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> 0
the store's clock drift (-10 to 10 percent)> 0
drift bound for the tables (0 to 10 percent)> 5
A times its lease from (send or receive)>
Cancelled.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> 0
the store's clock drift (-10 to 10 percent)> 0
drift bound for the tables (0 to 10 percent)> 5
A times its lease from (send or receive)> both
Type send or receive.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 7
margin (0 to 999 ms)>
Cancelled.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 7
margin (0 to 999 ms)> 1000
Type a whole number from 0 to 999.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 7
margin (0 to 999 ms)> -1
Type a whole number from 0 to 999.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 7
margin (0 to 999 ms)> x
Type a whole number from 0 to 999.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 7
margin (0 to 999 ms)> 500
Lease 1000 ms. A's delay to the store 30 ms each way, B's 10 ms.
A's clock drifts 0%, the store's 0%; the tables cover drifts within 5%.
A timing from when it asks; a margin of 500 ms, so A stops when its clock has counted 500 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 5
lease (100 to 5000 ms)> 400
The lease must be longer than the margin, 500 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 7
margin (0 to 999 ms)> 999
Lease 1000 ms. A's delay to the store 30 ms each way, B's 10 ms.
A's clock drifts 0%, the store's 0%; the tables cover drifts within 5%.
A timing from when it asks; a margin of 999 ms, so A stops when its clock has counted 1 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 2
One lease, A timing from when it asks:
0 ms A asks the store for the lease, and starts its timer
1 ms A's clock has counted 1 ms, the lease less the margin, before A has heard
30 ms the store grants it to A, for 1000 ms on the store's clock
60 ms A hears, but by its clock the lease is already over, so it never leads
1030 ms the store's clock has counted the lease: B's request is granted
1040 ms B hears, and acts as leader
No leader for 980 ms, from 60 to 1040 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 8
Bye.
What was typed (69 lines)
0
x
5
5
50
5
6000
5
x
5
1000
5
1000
101
5
1000
30
5
1000
30
-1
6
6
11
6
-11
6
x
6
0
6
0
0
6
0
0
11
6
0
0
5
6
0
0
5
both
7
7
1000
7
-1
7
x
7
500
5
400
7
999
2
8
basic
interpreter: byte-equal== Leader lease ==
A holds a lease from a store and then goes quiet; B takes over when the store's clock says the lease has run out, while A trusts its own clock.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 1
Lease 1000 ms. A's delay to the store 30 ms each way, B's 10 ms.
A's clock drifts 0%, the store's 0%; the tables cover drifts within 5%.
A timing from when it asks; a margin of 0 ms, so A stops when its clock has counted 1000 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 2
One lease, A timing from when it asks:
0 ms A asks the store for the lease, and starts its timer
30 ms the store grants it to A, for 1000 ms on the store's clock
60 ms A hears, and acts as leader
1000 ms A's clock has counted 1000 ms: A stops
1030 ms the store's clock has counted the lease: B's request is granted
1040 ms B hears, and acts as leader
No leader for 40 ms, from 1000 to 1040 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 3
Two leaders, in ms: A's clock drift down the side, the store's across; a margin of 0 ms, A timing from when it asks.
-5% -4% -3% -2% -1% 0% 1% 2% 3% 4% 5%
A -5% 0 0 0 0 2 13 22 32 42 51 60
A -4% 0 0 0 0 0 2 11 21 31 40 49
A -3% 0 0 0 0 0 0 0 10 20 29 38
A -2% 0 0 0 0 0 0 0 0 10 19 28
A -1% 0 0 0 0 0 0 0 0 0 9 18
A 0% 0 0 0 0 0 0 0 0 0 0 7
A 1% 0 0 0 0 0 0 0 0 0 0 0
A 2% 0 0 0 0 0 0 0 0 0 0 0
A 3% 0 0 0 0 0 0 0 0 0 0 0
A 4% 0 0 0 0 0 0 0 0 0 0 0
A 5% 0 0 0 0 0 0 0 0 0 0 0
Two leaders in 23 of the 121 pairs, for up to 60 ms; no leader for up to 140 ms.
A slow clock keeps A leading longer in real time, and a fast store frees the lease sooner.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 4
For drifts anywhere within 5%, A timing from when it asks:
The smallest margin with no two leaders for any of them is 57 ms; at that margin, no leader for up to 194 ms.
Each pair alone would need from 0 to 57 ms. The margin has to cover the worst pair, A's clock slow and the store's fast, and the others pay for it in time without a leader.
A timing from when it hears instead, the smallest such margin is 114 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> 0
the store's clock drift (-10 to 10 percent)> 0
drift bound for the tables (0 to 10 percent)> 5
A times its lease from (send or receive)> receive
Lease 1000 ms. A's delay to the store 30 ms each way, B's 10 ms.
A's clock drifts 0%, the store's 0%; the tables cover drifts within 5%.
A timing from when it hears; a margin of 0 ms, so A stops when its clock has counted 1000 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 2
One lease, A timing from when it hears:
0 ms A asks the store for the lease
30 ms the store grants it to A, for 1000 ms on the store's clock
60 ms A hears, starts its timer, and acts as leader
1030 ms the store's clock has counted the lease: B's request is granted
1040 ms B hears, and acts as leader
1060 ms A's clock has counted 1000 ms: A stops
Two leaders for 20 ms, from 1040 to 1060 ms: A still trusts its lease, and B holds the new one.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 4
For drifts anywhere within 5%, A timing from when it hears:
The smallest margin with no two leaders for any of them is 114 ms; at that margin, no leader for up to 189 ms.
Each pair alone would need from 0 to 114 ms. The margin has to cover the worst pair, A's clock slow and the store's fast, and the others pay for it in time without a leader.
A timing from when it asks instead, the smallest such margin is 57 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> -5
the store's clock drift (-10 to 10 percent)> 0
drift bound for the tables (0 to 10 percent)> 5
A times its lease from (send or receive)> send
Lease 1000 ms. A's delay to the store 30 ms each way, B's 10 ms.
A's clock drifts -5%, the store's 0%; the tables cover drifts within 5%.
A timing from when it asks; a margin of 0 ms, so A stops when its clock has counted 1000 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 2
One lease, A timing from when it asks:
0 ms A asks the store for the lease, and starts its timer
30 ms the store grants it to A, for 1000 ms on the store's clock
60 ms A hears, and acts as leader
1030 ms the store's clock has counted the lease: B's request is granted
1040 ms B hears, and acts as leader
1053 ms A's clock, running 5% slow, has counted 1000 ms: A stops
Two leaders for 13 ms, from 1040 to 1053 ms: A still trusts its lease, and B holds the new one.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 3
Two leaders, in ms: A's clock drift down the side, the store's across; a margin of 0 ms, A timing from when it asks.
-5% -4% -3% -2% -1% 0% 1% 2% 3% 4% 5%
A -5% 0 0 0 0 2 13 22 32 42 51 60
A -4% 0 0 0 0 0 2 11 21 31 40 49
A -3% 0 0 0 0 0 0 0 10 20 29 38
A -2% 0 0 0 0 0 0 0 0 10 19 28
A -1% 0 0 0 0 0 0 0 0 0 9 18
A 0% 0 0 0 0 0 0 0 0 0 0 7
A 1% 0 0 0 0 0 0 0 0 0 0 0
A 2% 0 0 0 0 0 0 0 0 0 0 0
A 3% 0 0 0 0 0 0 0 0 0 0 0
A 4% 0 0 0 0 0 0 0 0 0 0 0
A 5% 0 0 0 0 0 0 0 0 0 0 0
Two leaders in 23 of the 121 pairs, for up to 60 ms; no leader for up to 140 ms.
A slow clock keeps A leading longer in real time, and a fast store frees the lease sooner.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 7
margin (0 to 999 ms)> 57
Lease 1000 ms. A's delay to the store 30 ms each way, B's 10 ms.
A's clock drifts -5%, the store's 0%; the tables cover drifts within 5%.
A timing from when it asks; a margin of 57 ms, so A stops when its clock has counted 943 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 3
Two leaders, in ms: A's clock drift down the side, the store's across; a margin of 57 ms, A timing from when it asks.
-5% -4% -3% -2% -1% 0% 1% 2% 3% 4% 5%
A -5% 0 0 0 0 0 0 0 0 0 0 0
A -4% 0 0 0 0 0 0 0 0 0 0 0
A -3% 0 0 0 0 0 0 0 0 0 0 0
A -2% 0 0 0 0 0 0 0 0 0 0 0
A -1% 0 0 0 0 0 0 0 0 0 0 0
A 0% 0 0 0 0 0 0 0 0 0 0 0
A 1% 0 0 0 0 0 0 0 0 0 0 0
A 2% 0 0 0 0 0 0 0 0 0 0 0
A 3% 0 0 0 0 0 0 0 0 0 0 0
A 4% 0 0 0 0 0 0 0 0 0 0 0
A 5% 0 0 0 0 0 0 0 0 0 0 0
No two leaders in any of the 121 pairs; no leader for up to 194 ms.
A slow clock keeps A leading longer in real time, and a fast store frees the lease sooner.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 2
One lease, A timing from when it asks:
0 ms A asks the store for the lease, and starts its timer
30 ms the store grants it to A, for 1000 ms on the store's clock
60 ms A hears, and acts as leader
993 ms A's clock, running 5% slow, has counted 943 ms, the lease less the margin: A stops
1030 ms the store's clock has counted the lease: B's request is granted
1040 ms B hears, and acts as leader
No leader for 47 ms, from 993 to 1040 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 6
A's clock drift (-10 to 10 percent)> 0
the store's clock drift (-10 to 10 percent)> 0
drift bound for the tables (0 to 10 percent)> 10
A times its lease from (send or receive)> send
Lease 1000 ms. A's delay to the store 30 ms each way, B's 10 ms.
A's clock drifts 0%, the store's 0%; the tables cover drifts within 10%.
A timing from when it asks; a margin of 57 ms, so A stops when its clock has counted 943 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 4
For drifts anywhere within 10%, A timing from when it asks:
The smallest margin with no two leaders for any of them is 145 ms; at that margin, no leader for up to 374 ms.
Each pair alone would need from 0 to 145 ms. The margin has to cover the worst pair, A's clock slow and the store's fast, and the others pay for it in time without a leader.
A timing from when it hears instead, the smallest such margin is 199 ms.
1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit
choice> 8
Bye.
What was typed (29 lines)
1
2
3
4
6
0
0
5
receive
2
4
6
-5
0
5
send
2
3
7
57
3
2
6
0
0
10
send
4
8
Modules
The program as written, entry module first. Each module transpiles to its own Python file, which is what eml project run executes.
main.eml(entry)
eml# P120 leader lease: one lease from A to B in real time, two leaders over
# every pair of clock drifts, and the margin that removes them.
import lease
def plain(s):
0 => i
len(s) => j
while i < j and s[i] == " ":
i + 1 => i
while j > i and s[j - 1] == " ":
j - 1 => j
return s[i:j]
def pad(s, n):
s => out
while len(out) < n:
out + " " => out
return out
def lpad(s, n):
s => out
while len(out) < n:
" " + out => out
return out
def is_digits(s):
if len(s) == 0:
return False
for c in s:
if c < "0" or c > "9":
return False
return True
def timer_text(timer):
if timer == "send":
return "A timing from when it asks"
return "A timing from when it hears"
def drift_text(d):
if d > 0:
return ", running " + str(d) + "% fast,"
if d < 0:
return ", running " + str(0 - d) + "% slow,"
return ""
def show(st):
# st: [lease, A's delay, B's delay, A's drift, store's drift, bound, timer, margin]
("Lease " + str(st[0]) + " ms. A's delay to the store " + str(st[1]) + " ms each way, B's " + str(st[2]) + " ms.") ^0
("A's clock drifts " + str(st[3]) + "%, the store's " + str(st[4]) + "%; the tables cover drifts within " + str(st[5]) + "%.") ^0
(timer_text(st[6]) + "; a margin of " + str(st[7]) + " ms, so A stops when its clock has counted " + str(st[0] - st[7]) + " ms.") ^0
def one_lease(st):
lease.outcome(st[0], st[7], st[3], st[4], st[1], st[2], st[6]) => o
2 * st[1] => heard
lease.store_frees(st[0], st[4], st[1]) => frees
("One lease, " + timer_text(st[6]) + ":") ^0
[] => ev
if st[6] == "send":
ev + [[0, "A asks the store for the lease, and starts its timer"]] => ev
else:
ev + [[0, "A asks the store for the lease"]] => ev
ev + [[st[1], "the store grants it to A, for " + str(st[0]) + " ms on the store's clock"]] => ev
if o[2] <= heard:
ev + [[o[2], "A's clock" + drift_text(st[3]) + " has counted " + str(st[0] - st[7]) + " ms, the lease less the margin, before A has heard"]] => ev
ev + [[heard, "A hears, but by its clock the lease is already over, so it never leads"]] => ev
else:
if st[6] == "send":
ev + [[heard, "A hears, and acts as leader"]] => ev
else:
ev + [[heard, "A hears, starts its timer, and acts as leader"]] => ev
ev + [[o[2], stop_text(st)]] => ev
ev + [[frees, "the store's clock" + drift_text(st[4]) + " has counted the lease: B's request is granted"]] => ev
ev + [[o[3], "B hears, and acts as leader"]] => ev
# in order of time; events at the same ms keep their order
[] => ordered
for e in ev:
[] => out
False => placed
for x in ordered:
if not placed and e[0] < x[0]:
out + [e] => out
True => placed
out + [x] => out
if not placed:
out + [e] => out
out => ordered
for e in ordered:
(" " + lpad(str(e[0]), 6) + " ms " + e[1]) ^0
if o[0] > 0:
("Two leaders for " + str(o[0]) + " ms, from " + str(lease.max2(o[3], heard)) + " to " + str(o[2]) + " ms: A still trusts its lease, and B holds the new one.") ^0
elif o[1] > 0:
("No leader for " + str(o[1]) + " ms, from " + str(lease.max2(o[2], heard)) + " to " + str(o[3]) + " ms.") ^0
else:
"One leader at every moment: A stops just as B starts." ^0
def stop_text(st):
if st[7] == 0:
return "A's clock" + drift_text(st[3]) + " has counted " + str(st[0]) + " ms: A stops"
return "A's clock" + drift_text(st[3]) + " has counted " + str(st[0] - st[7]) + " ms, the lease less the margin: A stops"
def every(st):
lease.grid(st[0], st[7], st[5], st[1], st[2], st[6]) => g
("Two leaders, in ms: A's clock drift down the side, the store's across; a margin of " + str(st[7]) + " ms, " + timer_text(st[6]) + ".") ^0
" " + pad("", 8) => head
for s in [0 - st[5]:st[5]]:
head + lpad(str(s) + "%", 6) => head
head ^0
for row in g[0]:
" " + pad("A " + str(row[0]) + "%", 8) => line
for x in row[1]:
line + lpad(str(x), 6) => line
line ^0
(2 * st[5] + 1) * (2 * st[5] + 1) => pairs
if g[1][0] == 0:
("No two leaders in any of the " + str(pairs) + " pairs; no leader for up to " + str(g[1][2]) + " ms.") ^0
else:
("Two leaders in " + str(g[1][0]) + " of the " + str(pairs) + " pairs, for up to " + str(g[1][1]) + " ms; no leader for up to " + str(g[1][2]) + " ms.") ^0
if st[5] > 0:
"A slow clock keeps A leading longer in real time, and a fast store frees the lease sooner." ^0
def find(st):
lease.safe_margin(st[0], st[5], st[1], st[2], st[6]) => m
("For drifts anywhere within " + str(st[5]) + "%, " + timer_text(st[6]) + ":") ^0
if m[0] < 0:
" No margin shorter than the lease removes two leaders here." ^0
else:
(" The smallest margin with no two leaders for any of them is " + str(m[0]) + " ms; at that margin, no leader for up to " + str(m[3]) + " ms.") ^0
if m[1] < m[2]:
(" Each pair alone would need from " + str(m[1]) + " to " + str(m[2]) + " ms. The margin has to cover the worst pair, A's clock slow and the store's fast, and the others pay for it in time without a leader.") ^0
"receive" => other
if st[6] == "receive":
"send" => other
lease.safe_margin(st[0], st[5], st[1], st[2], other) => m2
if m2[0] < 0:
(" " + timer_text(other) + " instead, no margin shorter than the lease would do.") ^0
else:
(" " + timer_text(other) + " instead, the smallest such margin is " + str(m2[0]) + " ms.") ^0
def ask_int(prompt, low, high):
# [ok, value]; a cancel or a bad number says so and is not ok
plain(input(prompt)) => t
if t == "":
"Cancelled." ^0
return [False, 0]
1 => sign
t => digits
if t[0] == "-":
0 - 1 => sign
t[1:len(t)] => digits
if not is_digits(digits) or len(digits) > 4 or sign * int(digits) < low or sign * int(digits) > high:
("Type a whole number from " + str(low) + " to " + str(high) + ".") ^0
return [False, 0]
return [True, sign * int(digits)]
def lease_and_delays(st):
ask_int("lease (100 to 5000 ms)> ", 100, 5000) => l
if not l[0]:
return st
if l[1] <= st[7]:
("The lease must be longer than the margin, " + str(st[7]) + " ms.") ^0
return st
ask_int("A's delay to the store (0 to 100 ms)> ", 0, 100) => da
if not da[0]:
return st
ask_int("B's delay to the store (0 to 100 ms)> ", 0, 100) => db
if not db[0]:
return st
[l[1], da[1], db[1], st[3], st[4], st[5], st[6], st[7]] => out
show(out)
return out
def clocks(st):
ask_int("A's clock drift (-10 to 10 percent)> ", 0 - 10, 10) => a
if not a[0]:
return st
ask_int("the store's clock drift (-10 to 10 percent)> ", 0 - 10, 10) => s
if not s[0]:
return st
ask_int("drift bound for the tables (0 to 10 percent)> ", 0, 10) => b
if not b[0]:
return st
plain(input("A times its lease from (send or receive)> ")) => t
if t == "":
"Cancelled." ^0
return st
if t != "send" and t != "receive":
"Type send or receive." ^0
return st
[st[0], st[1], st[2], a[1], s[1], b[1], t, st[7]] => out
show(out)
return out
def margin(st):
ask_int("margin (0 to " + str(st[0] - 1) + " ms)> ", 0, st[0] - 1) => m
if not m[0]:
return st
[st[0], st[1], st[2], st[3], st[4], st[5], st[6], m[1]] => out
show(out)
return out
[1000, 30, 10, 0, 0, 5, "send", 0] => st
"== Leader lease ==" ^0
"A holds a lease from a store and then goes quiet; B takes over when the store's clock says the lease has run out, while A trusts its own clock." ^0
True => running
while running:
"" ^0
"1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit" ^0
plain(input("choice> ")) => choice
if choice == "1":
show(st)
elif choice == "2":
one_lease(st)
elif choice == "3":
every(st)
elif choice == "4":
find(st)
elif choice == "5":
lease_and_delays(st) => st
elif choice == "6":
clocks(st) => st
elif choice == "7":
margin(st) => st
elif choice == "8":
False => running
else:
"Pick a number from 1 to 8." ^0
"Bye." ^0
Python projection (main.py)
import lease
def plain(s):
i = 0
j = len(s)
while i < j and s[i] == " ":
i = i + 1
while j > i and s[j - 1] == " ":
j = j - 1
return s[i:j]
def pad(s, n):
out = s
while len(out) < n:
out = out + " "
return out
def lpad(s, n):
out = s
while len(out) < n:
out = " " + out
return out
def is_digits(s):
if len(s) == 0:
return False
for c in s:
if c < "0" or c > "9":
return False
return True
def timer_text(timer):
if timer == "send":
return "A timing from when it asks"
return "A timing from when it hears"
def drift_text(d):
if d > 0:
return ", running " + str(d) + "% fast,"
if d < 0:
return ", running " + str(0 - d) + "% slow,"
return ""
def show(st):
print("Lease " + str(st[0]) + " ms. A's delay to the store " + str(st[1]) + " ms each way, B's " + str(st[2]) + " ms.")
print("A's clock drifts " + str(st[3]) + "%, the store's " + str(st[4]) + "%; the tables cover drifts within " + str(st[5]) + "%.")
print(timer_text(st[6]) + "; a margin of " + str(st[7]) + " ms, so A stops when its clock has counted " + str(st[0] - st[7]) + " ms.")
def one_lease(st):
o = lease.outcome(st[0], st[7], st[3], st[4], st[1], st[2], st[6])
heard = 2 * st[1]
frees = lease.store_frees(st[0], st[4], st[1])
print("One lease, " + timer_text(st[6]) + ":")
ev = []
if st[6] == "send":
ev = ev + [[0, "A asks the store for the lease, and starts its timer"]]
else:
ev = ev + [[0, "A asks the store for the lease"]]
ev = ev + [[st[1], "the store grants it to A, for " + str(st[0]) + " ms on the store's clock"]]
if o[2] <= heard:
ev = ev + [[o[2], "A's clock" + drift_text(st[3]) + " has counted " + str(st[0] - st[7]) + " ms, the lease less the margin, before A has heard"]]
ev = ev + [[heard, "A hears, but by its clock the lease is already over, so it never leads"]]
else:
if st[6] == "send":
ev = ev + [[heard, "A hears, and acts as leader"]]
else:
ev = ev + [[heard, "A hears, starts its timer, and acts as leader"]]
ev = ev + [[o[2], stop_text(st)]]
ev = ev + [[frees, "the store's clock" + drift_text(st[4]) + " has counted the lease: B's request is granted"]]
ev = ev + [[o[3], "B hears, and acts as leader"]]
ordered = []
for e in ev:
out = []
placed = False
for x in ordered:
if not placed and e[0] < x[0]:
out = out + [e]
placed = True
out = out + [x]
if not placed:
out = out + [e]
ordered = out
for e in ordered:
print(" " + lpad(str(e[0]), 6) + " ms " + e[1])
if o[0] > 0:
print("Two leaders for " + str(o[0]) + " ms, from " + str(lease.max2(o[3], heard)) + " to " + str(o[2]) + " ms: A still trusts its lease, and B holds the new one.")
elif o[1] > 0:
print("No leader for " + str(o[1]) + " ms, from " + str(lease.max2(o[2], heard)) + " to " + str(o[3]) + " ms.")
else:
print("One leader at every moment: A stops just as B starts.")
def stop_text(st):
if st[7] == 0:
return "A's clock" + drift_text(st[3]) + " has counted " + str(st[0]) + " ms: A stops"
return "A's clock" + drift_text(st[3]) + " has counted " + str(st[0] - st[7]) + " ms, the lease less the margin: A stops"
def every(st):
g = lease.grid(st[0], st[7], st[5], st[1], st[2], st[6])
print("Two leaders, in ms: A's clock drift down the side, the store's across; a margin of " + str(st[7]) + " ms, " + timer_text(st[6]) + ".")
head = " " + pad("", 8)
for s in range(0 - st[5], st[5]+1):
head = head + lpad(str(s) + "%", 6)
print(head)
for row in g[0]:
line = " " + pad("A " + str(row[0]) + "%", 8)
for x in row[1]:
line = line + lpad(str(x), 6)
print(line)
pairs = (2 * st[5] + 1) * (2 * st[5] + 1)
if g[1][0] == 0:
print("No two leaders in any of the " + str(pairs) + " pairs; no leader for up to " + str(g[1][2]) + " ms.")
else:
print("Two leaders in " + str(g[1][0]) + " of the " + str(pairs) + " pairs, for up to " + str(g[1][1]) + " ms; no leader for up to " + str(g[1][2]) + " ms.")
if st[5] > 0:
print("A slow clock keeps A leading longer in real time, and a fast store frees the lease sooner.")
def find(st):
m = lease.safe_margin(st[0], st[5], st[1], st[2], st[6])
print("For drifts anywhere within " + str(st[5]) + "%, " + timer_text(st[6]) + ":")
if m[0] < 0:
print(" No margin shorter than the lease removes two leaders here.")
else:
print(" The smallest margin with no two leaders for any of them is " + str(m[0]) + " ms; at that margin, no leader for up to " + str(m[3]) + " ms.")
if m[1] < m[2]:
print(" Each pair alone would need from " + str(m[1]) + " to " + str(m[2]) + " ms. The margin has to cover the worst pair, A's clock slow and the store's fast, and the others pay for it in time without a leader.")
other = "receive"
if st[6] == "receive":
other = "send"
m2 = lease.safe_margin(st[0], st[5], st[1], st[2], other)
if m2[0] < 0:
print(" " + timer_text(other) + " instead, no margin shorter than the lease would do.")
else:
print(" " + timer_text(other) + " instead, the smallest such margin is " + str(m2[0]) + " ms.")
def ask_int(prompt, low, high):
t = plain(input(prompt))
if t == "":
print("Cancelled.")
return [False, 0]
sign = 1
digits = t
if t[0] == "-":
sign = 0 - 1
digits = t[1:len(t)]
if not is_digits(digits) or len(digits) > 4 or sign * int(digits) < low or sign * int(digits) > high:
print("Type a whole number from " + str(low) + " to " + str(high) + ".")
return [False, 0]
return [True, sign * int(digits)]
def lease_and_delays(st):
l = ask_int("lease (100 to 5000 ms)> ", 100, 5000)
if not l[0]:
return st
if l[1] <= st[7]:
print("The lease must be longer than the margin, " + str(st[7]) + " ms.")
return st
da = ask_int("A's delay to the store (0 to 100 ms)> ", 0, 100)
if not da[0]:
return st
db = ask_int("B's delay to the store (0 to 100 ms)> ", 0, 100)
if not db[0]:
return st
out = [l[1], da[1], db[1], st[3], st[4], st[5], st[6], st[7]]
show(out)
return out
def clocks(st):
a = ask_int("A's clock drift (-10 to 10 percent)> ", 0 - 10, 10)
if not a[0]:
return st
s = ask_int("the store's clock drift (-10 to 10 percent)> ", 0 - 10, 10)
if not s[0]:
return st
b = ask_int("drift bound for the tables (0 to 10 percent)> ", 0, 10)
if not b[0]:
return st
t = plain(input("A times its lease from (send or receive)> "))
if t == "":
print("Cancelled.")
return st
if t != "send" and t != "receive":
print("Type send or receive.")
return st
out = [st[0], st[1], st[2], a[1], s[1], b[1], t, st[7]]
show(out)
return out
def margin(st):
m = ask_int("margin (0 to " + str(st[0] - 1) + " ms)> ", 0, st[0] - 1)
if not m[0]:
return st
out = [st[0], st[1], st[2], st[3], st[4], st[5], st[6], m[1]]
show(out)
return out
st = [1000, 30, 10, 0, 0, 5, "send", 0]
print("== Leader lease ==")
print("A holds a lease from a store and then goes quiet; B takes over when the store's clock says the lease has run out, while A trusts its own clock.")
running = True
while running:
print("")
print("1) settings 2) one lease 3) every drift 4) find a margin 5) lease and delays 6) clocks 7) margin 8) quit")
choice = plain(input("choice> "))
if choice == "1":
show(st)
elif choice == "2":
one_lease(st)
elif choice == "3":
every(st)
elif choice == "4":
find(st)
elif choice == "5":
st = lease_and_delays(st)
elif choice == "6":
st = clocks(st)
elif choice == "7":
st = margin(st)
elif choice == "8":
running = False
else:
print("Pick a number from 1 to 8.")
print("Bye.")
lease.eml
eml# P120 leader lease - A holds a lease from a store, then goes quiet; B
# takes over when the store's clock says the lease has run out. A believes
# it leads until its own clock says so. As in the corpus case
# leader-lease-expiry, nobody is wrong about their own clock, and two
# leaders overlap when A's lease outlasts the store's in real time. A
# margin makes A stop early.
#
# Times are whole milliseconds of real time. A clock that drifts d percent
# counts (100 + d) ms for every 100 real ones. A's request reaches the
# store after A's delay, and the answer takes as long again; B is always
# asking, and hears after B's delay.
def ceil_div(p, q):
# the smallest whole number at least p / q, for q > 0
int(p / q) => f
while f * q < p:
f + 1 => f
while (f - 1) * q >= p:
f - 1 => f
return f
def floor_div(p, q):
ceil_div(p, q) => f
if f * q > p:
f - 1 => f
return f
def timer_start(da, timer):
# A counts its lease from when it asks, or from when it hears
if timer == "send":
return 0
return 2 * da
def a_stops(lease, margin, a, da, timer):
# the first real ms at which A's clock has counted the lease less the
# margin
return timer_start(da, timer) + ceil_div((lease - margin) * 100, 100 + a)
def store_frees(lease, s, da):
# the first real ms at which the store's clock has counted the lease
# since it granted it to A
return ceil_div(da * (100 + s) + lease * 100, 100 + s)
def b_starts(lease, s, da, db):
return store_frees(lease, s, da) + db
def outcome(lease, margin, a, s, da, db, timer):
# [ms with two leaders, ms with none, A stops, B starts]; A leads from
# when it hears, 2 * da
a_stops(lease, margin, a, da, timer) => ea
b_starts(lease, s, da, db) => sb
2 * da => heard
ea - max2(sb, heard) => two
sb - max2(ea, heard) => none
return [max2(two, 0), max2(none, 0), ea, sb]
def max2(x, y):
if x > y:
return x
return y
def smallest_margin(lease, a, s, da, db, timer):
# the smallest margin with no two leaders for these drifts, or -1 if
# none below the lease
max2(b_starts(lease, s, da, db), 2 * da) - timer_start(da, timer) => room
if room <= 0:
return 0 - 1
max2(0, lease - floor_div(room * (100 + a), 100)) => m
if m >= lease:
return 0 - 1
return m
def grid(lease, margin, bound, da, db, timer):
# rows of [A's drift, overlaps for the store's drifts -bound..bound],
# and [pairs with two leaders, most two, most none]
[] => rows
0 => pairs
0 => most_two
0 => most_none
for a in [0 - bound:bound]:
[] => cells
for s in [0 - bound:bound]:
outcome(lease, margin, a, s, da, db, timer) => o
cells + [o[0]] => cells
if o[0] > 0:
pairs + 1 => pairs
if o[0] > most_two:
o[0] => most_two
if o[1] > most_none:
o[1] => most_none
rows + [[a, cells]] => rows
return [rows, [pairs, most_two, most_none]]
def safe_margin(lease, bound, da, db, timer):
# [the smallest margin with no two leaders for any drifts within the
# bound (-1 if none), the smallest and largest margin a single pair
# needs, the most ms with no leader at the safe margin]
0 => worst
lease => least
for a in [0 - bound:bound]:
for s in [0 - bound:bound]:
smallest_margin(lease, a, s, da, db, timer) => m
if m < 0:
return [0 - 1, 0, 0, 0]
if m > worst:
m => worst
if m < least:
m => least
0 => gap
for a in [0 - bound:bound]:
for s in [0 - bound:bound]:
outcome(lease, worst, a, s, da, db, timer)[1] => g
if g > gap:
g => gap
return [worst, least, worst, gap]
Python projection (lease.py)
def ceil_div(p, q):
f = int(p / q)
while f * q < p:
f = f + 1
while (f - 1) * q >= p:
f = f - 1
return f
def floor_div(p, q):
f = ceil_div(p, q)
if f * q > p:
f = f - 1
return f
def timer_start(da, timer):
if timer == "send":
return 0
return 2 * da
def a_stops(lease, margin, a, da, timer):
return timer_start(da, timer) + ceil_div((lease - margin) * 100, 100 + a)
def store_frees(lease, s, da):
return ceil_div(da * (100 + s) + lease * 100, 100 + s)
def b_starts(lease, s, da, db):
return store_frees(lease, s, da) + db
def outcome(lease, margin, a, s, da, db, timer):
ea = a_stops(lease, margin, a, da, timer)
sb = b_starts(lease, s, da, db)
heard = 2 * da
two = ea - max2(sb, heard)
none = sb - max2(ea, heard)
return [max2(two, 0), max2(none, 0), ea, sb]
def max2(x, y):
if x > y:
return x
return y
def smallest_margin(lease, a, s, da, db, timer):
room = max2(b_starts(lease, s, da, db), 2 * da) - timer_start(da, timer)
if room <= 0:
return 0 - 1
m = max2(0, lease - floor_div(room * (100 + a), 100))
if m >= lease:
return 0 - 1
return m
def grid(lease, margin, bound, da, db, timer):
rows = []
pairs = 0
most_two = 0
most_none = 0
for a in range(0 - bound, bound+1):
cells = []
for s in range(0 - bound, bound+1):
o = outcome(lease, margin, a, s, da, db, timer)
cells = cells + [o[0]]
if o[0] > 0:
pairs = pairs + 1
if o[0] > most_two:
most_two = o[0]
if o[1] > most_none:
most_none = o[1]
rows = rows + [[a, cells]]
return [rows, [pairs, most_two, most_none]]
def safe_margin(lease, bound, da, db, timer):
worst = 0
least = lease
for a in range(0 - bound, bound+1):
for s in range(0 - bound, bound+1):
m = smallest_margin(lease, a, s, da, db, timer)
if m < 0:
return [0 - 1, 0, 0, 0]
if m > worst:
worst = m
if m < least:
least = m
gap = 0
for a in range(0 - bound, bound+1):
for s in range(0 - bound, bound+1):
g = outcome(lease, worst, a, s, da, db, timer)[1]
if g > gap:
gap = g
return [worst, least, worst, gap]