Skip to content

Commit 028f34d

Browse files
thawk105claude
andcommitted
feat(silo/trace): write_set lock-coverage assert (izanagi 後続段 3, D38)
writePhase の #if TRACE ブロックに lock 被覆 assert を追加。verifier が構造的に 見えない領域 (lock 獲得・被覆・torn read) を検証ビルドでのみ検出する。 - trace.hh: namespace izanagi_trace に thread_local shadow set (どのタプルを自 worker が CAS-lock したか) + emit_lock_violation ('X' 行)。全て #if TRACE ゆえ perf ビルドに一切残らない (観測者効果分離)。namespace 内に置くことで perf ビルドの nm ガード (izanagi_trace 部分文字列一致) が漏れを確定的に覆う。 - transaction.cc: lockWriteSet 入口で shadow を whole-set clear (per-txn 隔離)、 CAS 成功で record_lock。writePhase で 2 点検査 — 入口 (獲得被覆: 全非 INSERT が lock==1 かつ自 worker 保持) と各 storeRelease 直前 (保持継続: 早期 unlock 検出)。 違反ごとに X 行 (reason=not-locked-at-entry / lock-lost-before-write)。txid は writePhase スコープに hoist し X を同 txn の C/R/W と相関させる。unlockWriteSet 2 種と writePhase 末尾でも shadow を clear。 X 行は izanagi 側 verifier で Integrity.lock_coverage_violations に配線され verdict を indeterminate に倒す (torn read は版 stamp を信用不能にするため。cycle ではない)。 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
1 parent dff0f1e commit 028f34d

2 files changed

Lines changed: 104 additions & 15 deletions

File tree

cc/silo/transaction.cc

Lines changed: 79 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,13 @@ Status TxExecutor::delete_record(Storage s, std::string_view key) {
144144

145145
void TxExecutor::lockWriteSet() {
146146
Tidword expected, desired;
147+
#if TRACE
148+
// Per-txn lock-coverage shadow reset (D38, 裁定7). Unconditional whole-set
149+
// clear at entry makes per-txn isolation independent of any abort/retry exit
150+
// path (defense-in-depth; the real false-green guard is the raw-lock-bit check
151+
// in writePhase). #if TRACE only -> compiled out of the perf build (絶対規律1).
152+
izanagi_trace::clear_shadow();
153+
#endif
147154

148155
[[maybe_unused]] retry
149156
: for (auto itr = write_set_.begin(); itr != write_set_.end(); ++itr) {
@@ -163,8 +170,16 @@ void TxExecutor::lockWriteSet() {
163170
desired = expected;
164171
desired.lock = 1;
165172
if (compareExchange((*itr).rcdptr_->tidword_.obj_, expected.obj_,
166-
desired.obj_))
173+
desired.obj_)) {
174+
#if TRACE
175+
// This worker now holds the lock on this tuple (D38). On the skeleton
176+
// CAS-success path (not the coder edit surface = the conflict response
177+
// above), so a variant cannot suppress the record without also failing
178+
// the acquisition it is meant to prove.
179+
izanagi_trace::record_lock((*itr).rcdptr_);
180+
#endif
167181
break;
182+
}
168183
}
169184
}
170185
if (itr->op_ == OpType::UPDATE && itr->rcdptr_->tidword_.absent) {
@@ -344,6 +359,9 @@ void TxExecutor::unlockWriteSet() {
344359
desired.lock = 0;
345360
storeRelease((*itr).rcdptr_->tidword_.obj_, desired.obj_);
346361
}
362+
#if TRACE
363+
izanagi_trace::clear_shadow(); // abort/retry exit -> reset coverage shadow (D38, 裁定7)
364+
#endif
347365
}
348366

349367
void TxExecutor::unlockWriteSet(
@@ -357,6 +375,9 @@ void TxExecutor::unlockWriteSet(
357375
desired.lock = 0;
358376
storeRelease((*itr).rcdptr_->tidword_.obj_, desired.obj_);
359377
}
378+
#if TRACE
379+
izanagi_trace::clear_shadow(); // partial unlock (retry/abort) -> reset shadow (D38, 裁定7)
380+
#endif
360381
}
361382

362383
bool TxExecutor::validationPhase() { // Validation Phase
@@ -521,20 +542,37 @@ void TxExecutor::writePhase() {
521542
// key and the produced version id. read_set_/write_set_ are still intact
522543
// here (cleared at the end of writePhase). All data is CC-native -- no
523544
// verification-only tuple field is added (docs/ccbench-anatomy.md 4-5).
524-
{
525-
const std::uint64_t txid = izanagi_trace::next_txid();
526-
izanagi_trace::emit_commit(thid_, txid, maxtid.epoch, maxtid.tid);
527-
for (auto& re : read_set_) {
528-
const Tidword v = re.get_tidword();
529-
izanagi_trace::emit_read(thid_, txid, izanagi_trace::key_to_hex(re.key_),
530-
v.epoch, v.tid);
531-
}
532-
for (auto& we : write_set_) {
533-
const char op = (we.op_ == OpType::INSERT) ? 'I'
534-
: (we.op_ == OpType::DELETE) ? 'D'
535-
: 'U';
536-
izanagi_trace::emit_write(thid_, txid, izanagi_trace::key_to_hex(we.key_),
537-
op, maxtid.epoch, maxtid.tid);
545+
// txid is hoisted to writePhase scope (D38) so the per-storeRelease retention
546+
// check in the write loop below shares this txn's id (keeps X lines correlated
547+
// with this txn's C/R/W; a fresh next_txid() would orphan them).
548+
const std::uint64_t izanagi_txid = izanagi_trace::next_txid();
549+
izanagi_trace::emit_commit(thid_, izanagi_txid, maxtid.epoch, maxtid.tid);
550+
for (auto& re : read_set_) {
551+
const Tidword v = re.get_tidword();
552+
izanagi_trace::emit_read(thid_, izanagi_txid, izanagi_trace::key_to_hex(re.key_),
553+
v.epoch, v.tid);
554+
}
555+
for (auto& we : write_set_) {
556+
const char op = (we.op_ == OpType::INSERT) ? 'I'
557+
: (we.op_ == OpType::DELETE) ? 'D'
558+
: 'U';
559+
izanagi_trace::emit_write(thid_, izanagi_txid, izanagi_trace::key_to_hex(we.key_),
560+
op, maxtid.epoch, maxtid.tid);
561+
}
562+
// Entry lock-coverage check (D38, 裁定4 point 1 = acquisition coverage).
563+
// Every non-INSERT write must be covered, right now at writePhase entry, by a
564+
// lock THIS worker holds. Reads the live tidword.lock (ground truth in the
565+
// tuple) AND the shadow set (owner = us; tidword has no owner field). Emits X
566+
// (not-locked-at-entry) per uncovered write = catches lock-skip. INSERT excluded
567+
// (created lock=1/absent, covered by construction).
568+
for (auto& we : write_set_) {
569+
if (we.op_ == OpType::INSERT) continue;
570+
Tidword cur;
571+
cur.obj_ = loadAcquire(we.rcdptr_->tidword_.obj_);
572+
if (!cur.lock || !izanagi_trace::holds_lock(we.rcdptr_)) {
573+
izanagi_trace::emit_lock_violation(thid_, izanagi_txid,
574+
izanagi_trace::key_to_hex(we.key_),
575+
"not-locked-at-entry");
538576
}
539577
}
540578
#endif
@@ -548,6 +586,19 @@ void TxExecutor::writePhase() {
548586
// update and unlock
549587
switch ((*itr).op_) {
550588
case OpType::UPDATE: {
589+
#if TRACE
590+
// Retention check (D38, 裁定4 point 2): the lock must still be held right
591+
// before we write this tuple's data. An early unlock (lock released before
592+
// the memcpy) opens a torn-read window -> emit X (lock-lost-before-write).
593+
{
594+
Tidword cur;
595+
cur.obj_ = loadAcquire((*itr).rcdptr_->tidword_.obj_);
596+
if (!cur.lock)
597+
izanagi_trace::emit_lock_violation(
598+
thid_, izanagi_txid, izanagi_trace::key_to_hex((*itr).key_),
599+
"lock-lost-before-write");
600+
}
601+
#endif
551602
memcpy((*itr).rcdptr_->body_.get_val_ptr(), (*itr).body_.get_val_ptr(),
552603
(*itr).body_.get_val_size());
553604
storeRelease((*itr).rcdptr_->tidword_.obj_, maxtid.obj_);
@@ -559,6 +610,16 @@ void TxExecutor::writePhase() {
559610
break;
560611
}
561612
case OpType::DELETE: {
613+
#if TRACE
614+
{
615+
Tidword cur;
616+
cur.obj_ = loadAcquire((*itr).rcdptr_->tidword_.obj_);
617+
if (!cur.lock)
618+
izanagi_trace::emit_lock_violation(
619+
thid_, izanagi_txid, izanagi_trace::key_to_hex((*itr).key_),
620+
"lock-lost-before-write");
621+
}
622+
#endif
562623
maxtid.absent = true;
563624
// Return value intentionally ignored: a missing key still needs the
564625
// tid bump and gc_records_ push below.
@@ -574,6 +635,9 @@ void TxExecutor::writePhase() {
574635
}
575636
}
576637

638+
#if TRACE
639+
izanagi_trace::clear_shadow(); // success path -> reset coverage shadow (D38, 裁定7)
640+
#endif
577641
gc_records();
578642
read_set_.clear();
579643
write_set_.clear();

include/trace.hh

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@
3030
#include <fstream>
3131
#include <ios>
3232
#include <string>
33+
#include <unordered_set>
3334

3435
namespace izanagi_trace {
3536

@@ -94,6 +95,30 @@ inline void emit_write(std::size_t thid, std::uint64_t txid,
9495
<< ' ' << tid << '\n';
9596
}
9697

98+
// --- Lock-coverage shadow set (izanagi 後続段 3, D38) ---
99+
// Records which tuples THIS worker CAS-locked in lockWriteSet, so writePhase
100+
// can verify every written tuple is still covered by a lock this thread holds.
101+
// Verification-only: entirely inside `#if TRACE`, so the perf build has none of
102+
// it (絶対規律1). Kept in namespace izanagi_trace so the perf-build nm guard
103+
// (buildcache._has_trace_symbols = "izanagi_trace" substring) deterministically
104+
// covers any accidental leak of this TU's symbols (D38/OBS-1).
105+
inline std::unordered_set<const void*>& lock_shadow() {
106+
thread_local std::unordered_set<const void*> s;
107+
return s;
108+
}
109+
inline void record_lock(const void* rcd) { lock_shadow().insert(rcd); }
110+
inline void clear_shadow() { lock_shadow().clear(); }
111+
inline bool holds_lock(const void* rcd) { return lock_shadow().count(rcd) != 0; }
112+
113+
// A lock-coverage violation: writePhase wrote (or is about to write) a tuple
114+
// without holding its lock. reason in {not-locked-at-entry, lock-lost-before-write}.
115+
// The verifier maps X lines to Integrity.lock_coverage_violations -> indeterminate
116+
// (a torn-read window makes version stamps untrustworthy; not a cycle). D38.
117+
inline void emit_lock_violation(std::size_t thid, std::uint64_t txid,
118+
const std::string& key_hex, const char* reason) {
119+
stream(thid) << "X " << txid << ' ' << key_hex << ' ' << reason << '\n';
120+
}
121+
97122
} // namespace izanagi_trace
98123

99124
#endif // TRACE

0 commit comments

Comments
 (0)