Consistency Models — linearizability থেকে eventual ladder

লক্ষ্য: উপরের আদালত-তিনটার automation। একই engine তিনবার চলবে — শুধু constraint-set বদলাবে; রায়ের সাথে legal order (বা তার অনুপস্থিতি) প্রমাণ হিসেবে ছাপবে।

# consistency_checker.py — ছোট history-তে model-verdict + counterexample
from itertools import permutations

H2 = [
    dict(id="w1", client="A", kind="w", val=1, start=0, end=1),
    dict(id="r1", client="B", kind="r", seen=0, start=2, end=3),
    dict(id="r2", client="B", kind="r", seen=1, start=4, end=5),
]
H3 = [
    dict(id="w1", client="A", kind="w", val=5, start=0, end=1),
    dict(id="r1", client="B", kind="r", seen=5, start=2, end=3),
    dict(id="r2", client="B", kind="r", seen=0, start=4, end=5),
]


def program_edges(hist):
    """একই client-এর op-গুলোর মধ্যে per-process order edge"""
    by_c, edges = {}, set()
    for op in hist:
        by_c.setdefault(op["client"], []).append(op)
    for ops in by_c.values():
        ops = sorted(ops, key=lambda o: o["start"])
        for a, b in zip(ops, ops[1:]):
            edges.add((a["id"], b["id"]))
    return edges


def feasible(order, hist, realtime, edges):
    pos = {op["id"]: i for i, op in enumerate(order)}
    cur = 0                                     # register init = 0
    for op in order:                            # value-consistency
        if op["kind"] == "w":
            cur = op["val"]
        elif op["seen"] != cur:
            return False
    if realtime:                                # linearizability-শর্ত
        for a in hist:
            for b in hist:
                if a is not b and a["end"] <= b["start"] \
                   and pos[a["id"]] > pos[b["id"]]:
                    return False
    return all(pos[a] < pos[b] for a, b in edges)


def find_witness(hist, realtime, edges):
    assert len(hist) <= 7, "brute-force n<=7"
    for perm in permutations(range(len(hist))):
        order = [hist[i] for i in perm]
        if feasible(order, hist, realtime, edges):
            return [op["id"] for op in order]
    return None


def verdict(name, H):
    print(f"-- history {name} --")
    for op in H:
        what = f"w(x={op['val']})" if op["kind"] == "w" \
            else f"r(x)->{op['seen']}"
        print(f"  {op['id']} [{op['client']}] {what} "
              f"t={op['start']}..{op['end']}")
    edges = program_edges(H)
    lin = find_witness(H, True, edges)
    seq = find_witness(H, False, edges)
    show = lambda w: "[" + ", ".join(w) + "]" if w else None
    print(f"  linearizable : {'হ্যাঁ ' + show(lin) if lin else 'না'}")
    print(f"  sequential   : {'হ্যাঁ ' + show(seq) if seq else 'না'}")
    if not lin and seq:
        print(f"  morph: real-time ফেলেই legal {show(seq)}")
    if not seq:
        print("  কোনো permutation-ই value+order মানে না — causal-ও ভাঙা")
    print()


verdict("H2", H2)
verdict("H3", H3)

প্রত্যাশিত output:

-- history H2 --
  w1 [A] w(x=1) t=0..1
  r1 [B] r(x)->0 t=2..3
  r2 [B] r(x)->1 t=4..5
  linearizable : না
  sequential   : হ্যাঁ [r1, w1, r2]
  morph: real-time ফেলেই legal [r1, w1, r2]

-- history H3 --
  w1 [A] w(x=5) t=0..1
  r1 [B] r(x)->5 t=2..3
  r2 [B] r(x)->0 t=4..5
  linearizable : না
  sequential   : না
  কোনো permutation-ই value+order মানে না — causal-ও ভাঙা

H2-র witness-order খেয়াল করুন — read আগে, write পরে; এটাই sequential-এর অনুমোদিত সময়-ভ্রম। H3-তে per-process order (r5 আগে r0) এমন order দাবি করে যেখানে 5 লেখার আগে 0 ফেরত দেওয়া যায় — কোনো permutation পারে না। নিজে বাড়ান: (১) H1 যোগ করুন (w(1) → single fresh read) — তিন verdict-ই হ্যাঁ; (২) n=7-এ runtime মাপুন — factorial growth চোখে; (৩) read-from edges যোগ করে পূর্ণ causal-validator বানান।