Project P130
Lost update
Users reading, adding to and writing back one shared value by a schedule, with and without a version check: every order of their turns counted, and only the serial ones keep every update without the check.
2 modules · 2 recorded sessionstext-menu UI in the terminalupdated 2026-10-17
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
Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives. A write made from a value read before someone else's write throws that write away.
main.eml- the menu, the users, one schedule with and without a version check, every order counted, the amounts, and two or three usersupdate.eml- a user's turn, a run of a schedule, every order of the users' turns, and the counts
How each part works:
- As in the corpus case
lost-update-schedule, each user takes three turns: read, add, write. The value starts at 100; users add +10, +5 and -3. The value carries whose updates it holds, so a lost update is named even when the amounts would cancel out. - Without a check, an order loses an update exactly when one user's read and write enclose another user's write. Only the orders that run the users one after another keep every update: 18 of the 20 orders of two users lose one, and 1674 of the 1680 orders of three.
- With a version check, a write goes through only if nobody has written since its read; otherwise it is refused, and the user reads again and starts over. No order loses an update; two users need 18 writes done again over the 20 orders, three need 2970.
- Turns left when the schedule ends are taken by the users still going, lowest number first.
What is checked: menu choices 1 to 6; a schedule of user numbers, up to 30 turns; three amounts from -99 to 99, not 0; 2 or 3 users. An empty answer cancels.
Sessions: sessions/basic.in gives: - the users, then 1 1 1 2 2 2 (one after another) and 1 2 1 2 1 2, where user 1's update is lost without a check; - every order, for two and three users; - three users with 1 2 3 three times: two updates lost, two writes done again with the check.
sessions/bad-input.in gives: - menu choices 0 and x; - schedules: a cancel, 1 3, 1 x and 31 turns; - amounts: a cancel, two amounts, 0, x and 100, then 5 -5 3; - users: a cancel and 4, then 3, and a schedule that loses user 1's +5.
Built on the verified corpus case lost-update-schedule (a read, modify and write that loses another user's write when the steps interleave).
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== Lost update ==
Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 0
Pick a number from 1 to 6.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> x
Pick a number from 1 to 6.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule>
Cancelled.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 3
Type user numbers from 1 to 2, separated by spaces.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 x
Type user numbers from 1 to 2, separated by spaces.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
Up to 30 turns.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts>
Cancelled.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 10 5
Type three amounts.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 10 0 5
Each amount is a whole number from -99 to 99, not 0.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 10 x 5
Each amount is a whole number from -99 to 99, not 0.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 100 5 5
Each amount is a whole number from -99 to 99, not 0.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 5 -5 3
Users now add +5, -5 and +3.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 5
users (2 or 3)>
Cancelled.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 5
users (2 or 3)> 4
Type 2 or 3.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 5
users (2 or 3)> 3
Now 3 users.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 2
A schedule: whose turn it is, users 1 to 3, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 2 1 2 1 2 3 3 3
Without a check:
1 user 1 reads 100
2 user 2 reads 100
3 user 1 adds +5, making 105
4 user 2 adds -5, making 95
5 user 1 writes 105 over 100
6 user 2 writes 95 over 105
7 user 3 reads 95
8 user 3 adds +3, making 98
9 user 3 writes 98 over 95
ends at 98, where every update kept would make 103: user 1's update was lost, written over by a value read before it
With a version check:
1 user 1 reads 100
2 user 2 reads 100
3 user 1 adds +5, making 105
4 user 2 adds -5, making 95
5 user 1 writes 105 over 100
6 user 2 finds the version moved from 0 to 1: its write is refused, and it starts over
7 user 3 reads 105
8 user 3 adds +3, making 108
9 user 3 writes 108 over 105
10 then user 2 reads 108
11 then user 2 adds -5, making 103
12 then user 2 writes 103 over 108
ends at 103: every update kept
1 write refused and done again; 12 turns in all
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 6
Bye.
What was typed (31 lines)
0
x
2
2
1 3
2
1 x
2
1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
4
4
10 5
4
10 0 5
4
10 x 5
4
100 5 5
4
5 -5 3
5
5
4
5
3
2
1 2 1 2 1 2 3 3 3
6
basic
interpreter: byte-equal== Lost update ==
Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 1
The value starts at 100; user 1 adds +10, user 2 adds +5. Each user reads, adds, then writes: three turns.
Every update kept, it ends at 115.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 1 1 2 2 2
Without a check:
1 user 1 reads 100
2 user 1 adds +10, making 110
3 user 1 writes 110 over 100
4 user 2 reads 110
5 user 2 adds +5, making 115
6 user 2 writes 115 over 110
ends at 115: every update kept
With a version check:
1 user 1 reads 100
2 user 1 adds +10, making 110
3 user 1 writes 110 over 100
4 user 2 reads 110
5 user 2 adds +5, making 115
6 user 2 writes 115 over 110
ends at 115: every update kept
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 2 1 2 1 2
Without a check:
1 user 1 reads 100
2 user 2 reads 100
3 user 1 adds +10, making 110
4 user 2 adds +5, making 105
5 user 1 writes 110 over 100
6 user 2 writes 105 over 110
ends at 105, where every update kept would make 115: user 1's update was lost, written over by a value read before it
With a version check:
1 user 1 reads 100
2 user 2 reads 100
3 user 1 adds +10, making 110
4 user 2 adds +5, making 105
5 user 1 writes 110 over 100
6 user 2 finds the version moved from 0 to 1: its write is refused, and it starts over
7 then user 2 reads 110
8 then user 2 adds +5, making 115
9 then user 2 writes 115 over 110
ends at 115: every update kept
1 write refused and done again; 9 turns in all
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 3
2 users, 20 orders of their turns:
without a check: 18 lose an update
with a version check: 0 lose one; 18 writes refused and done again in all, at most 9 turns in one order
3 users, 1680 orders of their turns:
without a check: 1674 lose an update
with a version check: 0 lose one; 2970 writes refused and done again in all, at most 15 turns in one order
An order loses an update when one user's read and write enclose another user's write; run one after another, the users never lose one.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 5
users (2 or 3)> 3
Now 3 users.
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 2
A schedule: whose turn it is, users 1 to 3, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 2 3 1 2 3 1 2 3
Without a check:
1 user 1 reads 100
2 user 2 reads 100
3 user 3 reads 100
4 user 1 adds +10, making 110
5 user 2 adds +5, making 105
6 user 3 adds -3, making 97
7 user 1 writes 110 over 100
8 user 2 writes 105 over 110
9 user 3 writes 97 over 105
ends at 97, where every update kept would make 112: user 1's and user 2's updates were lost, written over by values read before them
With a version check:
1 user 1 reads 100
2 user 2 reads 100
3 user 3 reads 100
4 user 1 adds +10, making 110
5 user 2 adds +5, making 105
6 user 3 adds -3, making 97
7 user 1 writes 110 over 100
8 user 2 finds the version moved from 0 to 1: its write is refused, and it starts over
9 user 3 finds the version moved from 0 to 1: its write is refused, and it starts over
10 then user 2 reads 110
11 then user 2 adds +5, making 115
12 then user 2 writes 115 over 110
13 then user 3 reads 115
14 then user 3 adds -3, making 112
15 then user 3 writes 112 over 115
ends at 112: every update kept
2 writes refused and done again; 15 turns in all
1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit
choice> 6
Bye.
What was typed (11 lines)
1
2
1 1 1 2 2 2
2
1 2 1 2 1 2
3
5
3
2
1 2 3 1 2 3 1 2 3
6
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# P130 lost update: two or three users reading, adding and writing back
# one shared value by a schedule, with and without a version check, and
# every interleaving counted.
import update
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 lpad(s, n):
s => out
while len(out) < n:
" " + out => out
return out
def right_value(start, deltas):
start => r
for d in deltas:
r + d => r
return r
def show(start, deltas):
"" => line
for u in [0:len(deltas) - 1]:
if line != "":
line + ", " => line
line + "user " + str(u + 1) + " adds " + update.signed(deltas[u]) => line
("The value starts at " + str(start) + "; " + line + ". Each user reads, adds, then writes: three turns.") ^0
("Every update kept, it ends at " + str(right_value(start, deltas)) + ".") ^0
def one(start, deltas):
len(deltas) => n
("A schedule: whose turn it is, users 1 to " + str(n) + ", such as 1 2 1 2 1 2 (up to 30 turns).") ^0
plain(input("schedule> ")) => t
if t == "":
"Cancelled." ^0
return
[] => sched
"" => w
for c in t + " ":
if c == " ":
if w != "":
if len(w) != 1 or w[0] < "1" or w[0] > str(n):
("Type user numbers from 1 to " + str(n) + ", separated by spaces.") ^0
return
sched + [int(w) - 1] => sched
"" => w
else:
w + c => w
if len(sched) > 30:
"Up to 30 turns." ^0
return
right_value(start, deltas) => right
for checked in [False, True]:
update.run(start, deltas, sched, checked) => r
if checked:
"With a version check:" ^0
else:
"Without a check:" ^0
for k in [0:len(r[0]) - 1]:
r[0][k] => e
" " => mark
if k >= len(sched):
" then " => mark
(" " + lpad(str(k + 1), 2) + mark + "user " + str(e[0] + 1) + " " + e[1]) ^0
if len(r[4]) == 0:
(" ends at " + str(r[1]) + ": every update kept") ^0
else:
"" => who
for u in r[4]:
if who != "":
who + " and " => who
who + "user " + str(u + 1) + "'s" => who
if len(r[4]) == 1:
(" ends at " + str(r[1]) + ", where every update kept would make " + str(right) + ": " + who + " update was lost, written over by a value read before it") ^0
else:
(" ends at " + str(r[1]) + ", where every update kept would make " + str(right) + ": " + who + " updates were lost, written over by values read before them") ^0
if r[2] == 1:
(" 1 write refused and done again; " + str(r[3]) + " turns in all") ^0
elif r[2] > 1:
(" " + str(r[2]) + " writes refused and done again; " + str(r[3]) + " turns in all") ^0
def every(start, deltas):
for n in [2:3]:
[] => ds
for u in [0:n - 1]:
ds + [deltas[u]] => ds
update.census(start, ds, False) => a
update.census(start, ds, True) => b
(str(n) + " users, " + str(a[0]) + " orders of their turns:") ^0
(" without a check: " + str(a[1]) + " lose an update") ^0
(" with a version check: " + str(b[1]) + " lose one; " + str(b[2]) + " writes refused and done again in all, at most " + str(b[3]) + " turns in one order") ^0
"An order loses an update when one user's read and write enclose another user's write; run one after another, the users never lose one." ^0
def set_amounts(deltas):
("Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).") ^0
plain(input("amounts> ")) => t
if t == "":
"Cancelled." ^0
return deltas
[] => out
"" => w
for c in t + " ":
if c == " ":
if w != "":
1 => sign
w => d
if d[0] == "-":
0 - 1 => sign
d[1:len(d)] => d
True => digits
if len(d) == 0 or len(d) > 2:
False => digits
for ch in d:
if ch < "0" or ch > "9":
False => digits
if not digits:
"Each amount is a whole number from -99 to 99, not 0." ^0
return deltas
if int(d) == 0:
"Each amount is a whole number from -99 to 99, not 0." ^0
return deltas
out + [sign * int(d)] => out
"" => w
else:
w + c => w
if len(out) != 3:
"Type three amounts." ^0
return deltas
("Users now add " + update.signed(out[0]) + ", " + update.signed(out[1]) + " and " + update.signed(out[2]) + ".") ^0
return out
100 => start
[10, 5, 0 - 3] => deltas
2 => users
"== Lost update ==" ^0
"Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives." ^0
True => running
while running:
"" ^0
"1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit" ^0
plain(input("choice> ")) => choice
[] => ds
for u in [0:users - 1]:
ds + [deltas[u]] => ds
if choice == "1":
show(start, ds)
elif choice == "2":
one(start, ds)
elif choice == "3":
every(start, deltas)
elif choice == "4":
set_amounts(deltas) => deltas
elif choice == "5":
plain(input("users (2 or 3)> ")) => t
if t == "2" or t == "3":
int(t) => users
("Now " + t + " users.") ^0
elif t == "":
"Cancelled." ^0
else:
"Type 2 or 3." ^0
elif choice == "6":
False => running
else:
"Pick a number from 1 to 6." ^0
"Bye." ^0
Python projection (main.py)
import update
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 lpad(s, n):
out = s
while len(out) < n:
out = " " + out
return out
def right_value(start, deltas):
r = start
for d in deltas:
r = r + d
return r
def show(start, deltas):
line = ""
for u in range(0, len(deltas)):
if line != "":
line = line + ", "
line = line + "user " + str(u + 1) + " adds " + update.signed(deltas[u])
print("The value starts at " + str(start) + "; " + line + ". Each user reads, adds, then writes: three turns.")
print("Every update kept, it ends at " + str(right_value(start, deltas)) + ".")
def one(start, deltas):
n = len(deltas)
print("A schedule: whose turn it is, users 1 to " + str(n) + ", such as 1 2 1 2 1 2 (up to 30 turns).")
t = plain(input("schedule> "))
if t == "":
print("Cancelled.")
return
sched = []
w = ""
for c in t + " ":
if c == " ":
if w != "":
if len(w) != 1 or w[0] < "1" or w[0] > str(n):
print("Type user numbers from 1 to " + str(n) + ", separated by spaces.")
return
sched = sched + [int(w) - 1]
w = ""
else:
w = w + c
if len(sched) > 30:
print("Up to 30 turns.")
return
right = right_value(start, deltas)
for checked in [False, True]:
r = update.run(start, deltas, sched, checked)
if checked:
print("With a version check:")
else:
print("Without a check:")
for k in range(0, len(r[0])):
e = r[0][k]
mark = " "
if k >= len(sched):
mark = " then "
print(" " + lpad(str(k + 1), 2) + mark + "user " + str(e[0] + 1) + " " + e[1])
if len(r[4]) == 0:
print(" ends at " + str(r[1]) + ": every update kept")
else:
who = ""
for u in r[4]:
if who != "":
who = who + " and "
who = who + "user " + str(u + 1) + "'s"
if len(r[4]) == 1:
print(" ends at " + str(r[1]) + ", where every update kept would make " + str(right) + ": " + who + " update was lost, written over by a value read before it")
else:
print(" ends at " + str(r[1]) + ", where every update kept would make " + str(right) + ": " + who + " updates were lost, written over by values read before them")
if r[2] == 1:
print(" 1 write refused and done again; " + str(r[3]) + " turns in all")
elif r[2] > 1:
print(" " + str(r[2]) + " writes refused and done again; " + str(r[3]) + " turns in all")
def every(start, deltas):
for n in range(2, 4):
ds = []
for u in range(0, n):
ds = ds + [deltas[u]]
a = update.census(start, ds, False)
b = update.census(start, ds, True)
print(str(n) + " users, " + str(a[0]) + " orders of their turns:")
print(" without a check: " + str(a[1]) + " lose an update")
print(" with a version check: " + str(b[1]) + " lose one; " + str(b[2]) + " writes refused and done again in all, at most " + str(b[3]) + " turns in one order")
print("An order loses an update when one user's read and write enclose another user's write; run one after another, the users never lose one.")
def set_amounts(deltas):
print("Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).")
t = plain(input("amounts> "))
if t == "":
print("Cancelled.")
return deltas
out = []
w = ""
for c in t + " ":
if c == " ":
if w != "":
sign = 1
d = w
if d[0] == "-":
sign = 0 - 1
d = d[1:len(d)]
digits = True
if len(d) == 0 or len(d) > 2:
digits = False
for ch in d:
if ch < "0" or ch > "9":
digits = False
if not digits:
print("Each amount is a whole number from -99 to 99, not 0.")
return deltas
if int(d) == 0:
print("Each amount is a whole number from -99 to 99, not 0.")
return deltas
out = out + [sign * int(d)]
w = ""
else:
w = w + c
if len(out) != 3:
print("Type three amounts.")
return deltas
print("Users now add " + update.signed(out[0]) + ", " + update.signed(out[1]) + " and " + update.signed(out[2]) + ".")
return out
start = 100
deltas = [10, 5, 0 - 3]
users = 2
print("== Lost update ==")
print("Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives.")
running = True
while running:
print("")
print("1) the users 2) one schedule 3) every order 4) amounts 5) two or three users 6) quit")
choice = plain(input("choice> "))
ds = []
for u in range(0, users):
ds = ds + [deltas[u]]
if choice == "1":
show(start, ds)
elif choice == "2":
one(start, ds)
elif choice == "3":
every(start, deltas)
elif choice == "4":
deltas = set_amounts(deltas)
elif choice == "5":
t = plain(input("users (2 or 3)> "))
if t == "2" or t == "3":
users = int(t)
print("Now " + t + " users.")
elif t == "":
print("Cancelled.")
else:
print("Type 2 or 3.")
elif choice == "6":
running = False
else:
print("Pick a number from 1 to 6.")
print("Bye.")
update.eml
eml# P130 lost update - users each read a shared value, add their own amount,
# and write it back, one step a turn as a schedule says. As in the corpus
# case lost-update-schedule, a write made from a value read before someone
# else's write throws that write away. With a version check, a write goes
# through only if nobody has written since its read; otherwise the user
# reads again and starts over.
#
# A user's state is [step, value read, version read, whose updates the value
# read holds]; step 0 reads, 1 adds, 2 writes, 3 is done. The shared value
# is [value, version, whose updates it holds].
def new_state(n):
[] => out
for i in [1:n]:
out + [[0, 0, 0, []]] => out
return out
def turn(users, shared, u, deltas, checked):
# one turn for user u: [what happened]; users and shared change in place
users[u] => s
if s[0] == 0:
shared[0] => s[1]
shared[1] => s[2]
shared[2] => s[3]
1 => s[0]
return "reads " + str(s[1])
if s[0] == 1:
s[1] + deltas[u] => s[1]
2 => s[0]
return "adds " + signed(deltas[u]) + ", making " + str(s[1])
if s[0] == 2:
if checked and shared[1] != s[2]:
0 => s[0]
return "finds the version moved from " + str(s[2]) + " to " + str(shared[1]) + ": its write is refused, and it starts over"
shared[0] => old
s[1] => shared[0]
shared[1] + 1 => shared[1]
s[3] + [u] => shared[2]
3 => s[0]
return "writes " + str(s[1]) + " over " + str(old)
return "is done"
def signed(n):
if n < 0:
return str(n)
return "+" + str(n)
def run(start, deltas, schedule, checked):
# [trace of [user, what], final value, refused writes, turns used, whose
# updates are lost]: the schedule, then every user still going, lowest
# first, until all done
len(deltas) => n
new_state(n) => users
[start, 0, []] => shared
[] => trace
0 => refused
for u in schedule:
turn(users, shared, u, deltas, checked) => w
trace + [[u, w]] => trace
if len(w) > 5 and w[0:5] == "finds":
refused + 1 => refused
True => going
0 => extra
while going and extra < 200:
False => going
for u in [0:n - 1]:
if not going and users[u][0] < 3:
turn(users, shared, u, deltas, checked) => w
trace + [[u, w]] => trace
if len(w) > 5 and w[0:5] == "finds":
refused + 1 => refused
True => going
extra + 1 => extra
[] => lost
for u in [0:n - 1]:
False => kept
for v in shared[2]:
if v == u:
True => kept
if not kept:
lost + [u] => lost
return [trace, shared[0], refused, len(trace), lost]
def interleavings(n):
# every order of n users' three turns
[] => counts
for i in [1:n]:
counts + [3] => counts
[[[], counts]] => todo
[] => out
while len(todo) > 0:
todo[len(todo) - 1] => item
todo[0:len(todo) - 1] => todo
0 => left
for c in item[1]:
left + c => left
if left == 0:
out + [item[0]] => out
else:
for u in [0:n - 1]:
if item[1][u] > 0:
[] => nc
for v in [0:n - 1]:
if v == u:
nc + [item[1][v] - 1] => nc
else:
nc + [item[1][v]] => nc
todo + [[item[0] + [u], nc]] => todo
return out
def census(start, deltas, checked):
# over every interleaving: [orders, orders losing an update, refused
# writes in all, the most turns any order needs]
0 => lost
0 => refused
0 => most
interleavings(len(deltas)) => orders
for o in orders:
run(start, deltas, o, checked) => r
if len(r[4]) > 0:
lost + 1 => lost
refused + r[2] => refused
if r[3] > most:
r[3] => most
return [len(orders), lost, refused, most]
Python projection (update.py)
def new_state(n):
out = []
for i in range(1, n+1):
out = out + [[0, 0, 0, []]]
return out
def turn(users, shared, u, deltas, checked):
s = users[u]
if s[0] == 0:
s[1] = shared[0]
s[2] = shared[1]
s[3] = shared[2]
s[0] = 1
return "reads " + str(s[1])
if s[0] == 1:
s[1] = s[1] + deltas[u]
s[0] = 2
return "adds " + signed(deltas[u]) + ", making " + str(s[1])
if s[0] == 2:
if checked and shared[1] != s[2]:
s[0] = 0
return "finds the version moved from " + str(s[2]) + " to " + str(shared[1]) + ": its write is refused, and it starts over"
old = shared[0]
shared[0] = s[1]
shared[1] = shared[1] + 1
shared[2] = s[3] + [u]
s[0] = 3
return "writes " + str(s[1]) + " over " + str(old)
return "is done"
def signed(n):
if n < 0:
return str(n)
return "+" + str(n)
def run(start, deltas, schedule, checked):
n = len(deltas)
users = new_state(n)
shared = [start, 0, []]
trace = []
refused = 0
for u in schedule:
w = turn(users, shared, u, deltas, checked)
trace = trace + [[u, w]]
if len(w) > 5 and w[0:5] == "finds":
refused = refused + 1
going = True
extra = 0
while going and extra < 200:
going = False
for u in range(0, n):
if not going and users[u][0] < 3:
w = turn(users, shared, u, deltas, checked)
trace = trace + [[u, w]]
if len(w) > 5 and w[0:5] == "finds":
refused = refused + 1
going = True
extra = extra + 1
lost = []
for u in range(0, n):
kept = False
for v in shared[2]:
if v == u:
kept = True
if not kept:
lost = lost + [u]
return [trace, shared[0], refused, len(trace), lost]
def interleavings(n):
counts = []
for i in range(1, n+1):
counts = counts + [3]
todo = [[[], counts]]
out = []
while len(todo) > 0:
item = todo[len(todo) - 1]
todo = todo[0:len(todo) - 1]
left = 0
for c in item[1]:
left = left + c
if left == 0:
out = out + [item[0]]
else:
for u in range(0, n):
if item[1][u] > 0:
nc = []
for v in range(0, n):
if v == u:
nc = nc + [item[1][v] - 1]
else:
nc = nc + [item[1][v]]
todo = todo + [[item[0] + [u], nc]]
return out
def census(start, deltas, checked):
lost = 0
refused = 0
most = 0
orders = interleavings(len(deltas))
for o in orders:
r = run(start, deltas, o, checked)
if len(r[4]) > 0:
lost = lost + 1
refused = refused + r[2]
if r[3] > most:
most = r[3]
return [len(orders), lost, refused, most]