检查和动作要不要在一起
贯穿 n07 的程序(一个小仓库),每行标了它碰的数据:
1 total = total + amount # 共享 total,写
2 log = [] # 本地
3 log.append("入库") # 本地
4 if stock >= need: # 共享 stock,读(检查)
5 stock = stock - need # 共享 stock,写(动作)
6 count = count + 1 # 共享 count,写
7 print(total) # 共享 total,只读
8 name = name.upper() # 本地第 4、5 行是检查-再-动作。分开锁(各锁各的)和合起来锁(一把锁包住两行),用模拟器比:
def inc_steps(k=1):
return [("read",), ("add", k), ("write",)]
def check_act_steps(need=1):
return [("read",), ("check", need), ("add", -need), ("write",)]
def run_schedule(threads, schedule, start=0):
"""threads: 每条线程是「步」的列表;schedule: 线程编号的序列,每个编号出现一次就走一步。
共享变量 n;每条线程有自己的寄存器 reg。交回 (最终 n, 记录列表)。"""
n = start
pc = [0] * len(threads)
reg = [0] * len(threads)
log = []
for t in schedule:
if pc[t] >= len(threads[t]):
continue
step = threads[t][pc[t]]
pc[t] += 1
n, reg[t], note, go_on = do_step(step, n, reg[t])
log.append("T" + str(t) + ":" + note)
if not go_on:
pc[t] = len(threads[t]) # 检查没过:这条线程后面的步全部跳过
return n, log
def do_step(step, n, r):
if step[0] == "read":
return n, n, "read " + str(n), True
if step[0] == "add":
return n, r + step[1], "add→" + str(r + step[1]), True
if step[0] == "write":
return r, r, "write " + str(r), True
if step[0] == "check":
ok = r >= step[1]
return n, r, "check " + str(r) + (">=" if ok else "<") + str(step[1]), ok
if step[0] == "atomic":
notes = []
ok = True
for s in step[1]:
n, r, note, ok = do_step(s, n, r)
notes.append(note)
if not ok:
break
return n, r, "atomic(" + ",".join(notes) + ")", ok
raise ValueError(step[0])
def all_schedules(a, b):
"""两条线程(a 步和 b 步)的全部交错:每个交错是一串 0/1。"""
if a == 0:
return [[1] * b]
if b == 0:
return [[0] * a]
return [[0] + s for s in all_schedules(a - 1, b)] + [[1] + s for s in all_schedules(a, b - 1)]
def outcomes(threads, start=0):
counts = {}
for s in all_schedules(len(threads[0]), len(threads[1])):
n, _ = run_schedule(threads, s, start)
counts[n] = counts.get(n, 0) + 1
return counts
def locked(steps):
return [("atomic", steps)]
sep = locked([("read",), ("check", 1)]) + locked([("add", -1), ("write",)])
together = locked(check_act_steps())
def sold(threads):
c = 0
for s in all_schedules(len(threads[0]), len(threads[1])):
n, log = run_schedule(threads, s, 1)
if sum(1 for x in log if "write" in x) > 1:
c += 1
return c
print(str(sold([sep, list(sep)])) + "/" + str(sold([together, list(together)])))
全部评论