Skip to content

Commit a3302bb

Browse files
the-mikedavisthe-mikedavis
authored
Merge pull request #311 from amazon-mq/p/anchor-before-first-fragment
Add a P model of the anchor-before-first-fragment cleanup design
2 parents bad78b7 + 3e8a1a8 commit a3302bb

10 files changed

Lines changed: 547 additions & 0 deletions

File tree

‎.github/workflows/p-model-check.yaml‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ jobs:
3030
gc_reset_multinode: ${{ steps.filter.outputs.gc_reset_multinode }}
3131
gc_leading_group: ${{ steps.filter.outputs.gc_leading_group }}
3232
gc_reset_leading_group: ${{ steps.filter.outputs.gc_reset_leading_group }}
33+
delete_stream_anchor: ${{ steps.filter.outputs.delete_stream_anchor }}
3334
read_resolution: ${{ steps.filter.outputs.read_resolution }}
3435
trimmed_segment: ${{ steps.filter.outputs.trimmed_segment }}
3536
orphan_leak: ${{ steps.filter.outputs.orphan_leak }}
@@ -52,11 +53,13 @@ jobs:
5253
echo "gc_reset_multinode=false" >> "$GITHUB_OUTPUT"
5354
echo "gc_leading_group=false" >> "$GITHUB_OUTPUT"
5455
echo "gc_reset_leading_group=false" >> "$GITHUB_OUTPUT"
56+
echo "delete_stream_anchor=false" >> "$GITHUB_OUTPUT"
5557
echo "read_resolution=false" >> "$GITHUB_OUTPUT"
5658
echo "$CHANGED" | grep -q '^p/gc-reset/' && echo "gc_reset=true" >> "$GITHUB_OUTPUT" || true
5759
echo "$CHANGED" | grep -q '^p/gc-reset-multinode/' && echo "gc_reset_multinode=true" >> "$GITHUB_OUTPUT" || true
5860
echo "$CHANGED" | grep -q '^p/gc-leading-group/' && echo "gc_leading_group=true" >> "$GITHUB_OUTPUT" || true
5961
echo "$CHANGED" | grep -q '^p/gc-reset-leading-group/' && echo "gc_reset_leading_group=true" >> "$GITHUB_OUTPUT" || true
62+
echo "$CHANGED" | grep -q '^p/delete-stream-anchor/' && echo "delete_stream_anchor=true" >> "$GITHUB_OUTPUT" || true
6063
echo "$CHANGED" | grep -q '^p/read-resolution/' && echo "read_resolution=true" >> "$GITHUB_OUTPUT" || true
6164
echo "trimmed_segment=false" >> "$GITHUB_OUTPUT"
6265
echo "$CHANGED" | grep -q '^p/trimmed-segment/' && echo "trimmed_segment=true" >> "$GITHUB_OUTPUT" || true
@@ -71,6 +74,7 @@ jobs:
7174
echo "gc_reset_multinode=true" >> "$GITHUB_OUTPUT"
7275
echo "gc_leading_group=true" >> "$GITHUB_OUTPUT"
7376
echo "gc_reset_leading_group=true" >> "$GITHUB_OUTPUT"
77+
echo "delete_stream_anchor=true" >> "$GITHUB_OUTPUT"
7478
echo "read_resolution=true" >> "$GITHUB_OUTPUT"
7579
echo "trimmed_segment=true" >> "$GITHUB_OUTPUT"
7680
echo "orphan_leak=true" >> "$GITHUB_OUTPUT"
@@ -275,6 +279,59 @@ jobs:
275279
echo "Gate satisfied: the offset-only re-check deletes the live leading group."
276280
echo "::endgroup::"
277281
282+
delete-stream-anchor:
283+
needs: changes
284+
if: needs.changes.outputs.delete_stream_anchor == 'true' || github.event_name == 'schedule'
285+
runs-on: ubuntu-latest
286+
steps:
287+
- uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
288+
- uses: actions/setup-dotnet@9a946fdbd5fb07b82b2f5a4466058b876ab72bb2 # v5.3.0
289+
with:
290+
dotnet-version: '8.0.x'
291+
- name: Install the P checker
292+
run: |
293+
dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
294+
echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
295+
- name: Compile
296+
run: |
297+
cd p/delete-stream-anchor
298+
p compile
299+
- name: Tests that must hold
300+
run: |
301+
cd p/delete-stream-anchor
302+
for tc in tcAnchorReclaimsAcrossCrash tcAnchorExplore; do
303+
echo "::group::$tc (expect hold)"
304+
p check -tc "$tc" -i 5000
305+
echo "::endgroup::"
306+
done
307+
# PCT surfaces rare interleavings the random strategy misses.
308+
echo "::group::tcAnchorExplore (PCT)"
309+
p check -tc tcAnchorExplore --sch-pct 10 -i 5000
310+
echo "::endgroup::"
311+
- name: Validation gate (a stale read or out-of-order anchor must reap live data)
312+
run: |
313+
cd p/delete-stream-anchor
314+
# Both MUST fail with the NOREAPLIVE counterexample. A green here means
315+
# the model no longer reaches the live-data reap, i.e. the consistent-read
316+
# or anchor-before-fragment requirement is no longer load-bearing in the
317+
# model and the by-construction result is not trustworthy.
318+
for tc in tcAnchorStaleReadReapsLive tcAnchorOrderingViolated; do
319+
rm -rf PCheckerOutput/
320+
echo "::group::$tc (expect the live-reap counterexample)"
321+
if p check -tc "$tc" -i 2000; then
322+
echo "ERROR: $tc passed; the model no longer reaps live data."
323+
echo "A stale anchor read (or a fragment written before the anchor) must reap a live"
324+
echo "stream, otherwise the consistent-read / ordering requirement is not load-bearing."
325+
exit 1
326+
fi
327+
if ! grep -rqF 'INV NOREAPLIVE violated' PCheckerOutput/BugFinding/; then
328+
echo "ERROR: $tc failed, but not with the expected NOREAPLIVE counterexample."
329+
exit 1
330+
fi
331+
echo "Gate satisfied: $tc reaps live data as expected."
332+
echo "::endgroup::"
333+
done
334+
278335
read-resolution:
279336
needs: changes
280337
if: needs.changes.outputs.read_resolution == 'true' || github.event_name == 'schedule'

‎p/delete-stream-anchor/PSpec/Monitors.p‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
/* Global safety monitors for the anchor-before-first-fragment design.
2+
3+
NoReapLive is the headline: a reap may happen only after the queue is deleted.
4+
It catches both load-bearing failures - a stale anchor read and an
5+
anchor-written-after-the-fragment ordering violation each cause the sweep to
6+
reap a live stream, which trips here. EventuallyEmpty is the by-construction
7+
reclaim: once the stream is deleted and sweeps quiesce, no object remains, even
8+
across a crash mid-sweep. */
9+
10+
/* A reap is legitimate only for a deleted stream. */
11+
spec NoReapLive observes eQueueDeleted, eObjReaped {
12+
var queueDeleted: bool;
13+
14+
start state Watching {
15+
on eQueueDeleted do {
16+
queueDeleted = true;
17+
}
18+
on eObjReaped do (k: ObjKey) {
19+
assert queueDeleted,
20+
format("INV NOREAPLIVE violated: GC reaped object (offset={0}, uid={1}) while the stream's queue is still live (the anchor read was stale, or the anchor was written after the fragment)",
21+
k.offset, k.uid);
22+
}
23+
}
24+
}
25+
26+
/* Once the stream is deleted and sweeps quiesce, nothing is left under the prefix. */
27+
spec EventuallyEmpty observes eObjStored, eObjReaped, eSweepQuiesced {
28+
var stored: map[ObjKey, bool];
29+
30+
start state Watching {
31+
on eObjStored do (k: ObjKey) {
32+
if (!(k in stored)) {
33+
stored += (k, true);
34+
}
35+
}
36+
on eObjReaped do (k: ObjKey) {
37+
if (k in stored) {
38+
stored -= (k);
39+
}
40+
}
41+
on eSweepQuiesced do {
42+
assert sizeof(stored) == 0,
43+
format("INV RECLAIM violated: {0} object(s) left under the prefix after the stream was deleted and sweeps quiesced",
44+
sizeof(stored));
45+
}
46+
}
47+
}

‎p/delete-stream-anchor/PSrc/Common.p‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
/* Shared types and events for the anchor-before-first-fragment cleanup design.
2+
3+
The design:
4+
5+
- Before the very first S3 fragment is written for a stream, the replica
6+
reader writes a dedicated ANCHOR node in Khepri, keep_while'd to the queue,
7+
as a BLOCKING step. The anchor's write must COMMIT strictly before the
8+
first S3 PUT.
9+
- Cleanup is driven by the anchor's ABSENCE, not by any record written at
10+
deletion time. The keep_while removes the anchor in the same transaction
11+
that deletes the queue, so "anchor absent" is produced atomically and is
12+
permanent. A sweep classifies the prefix as junk iff objects are present
13+
AND the anchor is absent.
14+
15+
This is correct by construction off one ordering invariant: an object exists
16+
only after the anchor committed, and the anchor disappears only when the queue
17+
does, so there is NO live state with objects-but-no-anchor. Two properties
18+
fall out for free: a stream that never committed a manifest still has an
19+
anchor (it predates the first fragment), and a crash anywhere in the deletion
20+
path cannot lose the signal (the signal is the anchor's permanent absence, not
21+
a write that can be dropped).
22+
23+
TWO things are load-bearing, and this model exists to prove both:
24+
25+
1. CONSISTENT READS. The sweep must read the anchor with a strongly-consistent
26+
(committed) read. A stale local replica can report "anchor absent" for a
27+
stream whose anchor just committed while S3 already shows its first
28+
fragment, and a stale-read sweep then reaps LIVE data. (Same shape as the
29+
gc-reset-multinode stale-floor finding.)
30+
31+
2. ORDERING. The anchor must commit BEFORE the first fragment PUT. If a
32+
fragment can exist before the anchor commits, a sweep in that window sees
33+
objects-but-no-anchor for a LIVE stream and reaps it, even with consistent
34+
reads. */
35+
36+
/* An S3 object under the stream's prefix, identified by (offset, uid). One
37+
stream is modeled; every object here belongs to that stream's prefix. */
38+
type ObjKey = (offset: int, uid: int);
39+
40+
/* S3 object store (the stream's prefix). */
41+
event eS3Put: (from: machine, key: ObjKey);
42+
event eS3DeleteAll: (from: machine);
43+
event eS3List: (from: machine);
44+
event eS3ListResult: int;
45+
event eS3Ack;
46+
47+
/* Khepri: the committed truth (queue + anchor) plus a lagging local replica
48+
cache. A consistent read returns the committed anchor; a local read returns the
49+
cached anchor, which may be stale. */
50+
event eWriteAnchor: (from: machine);
51+
event eReplicate: (from: machine);
52+
event eDeleteQueue: (from: machine);
53+
event eReadAnchor: (from: machine, consistent: bool);
54+
event eAnchorResult: bool;
55+
event eKAck;
56+
57+
/* Writer / replica reader: ensure the anchor, then PUT the first fragment.
58+
anchorBeforeFragment selects whether the load-bearing ordering is honored. */
59+
event eEnsureAnchorThenPut: (from: machine, key: ObjKey, anchorBeforeFragment: bool);
60+
event eWriterDone;
61+
62+
/* GC sweep: list the prefix, read the anchor, reap iff objects present and anchor
63+
absent. consistent selects the read mode; crashBeforeDelete drops the reap to
64+
model a crash mid-sweep (the next sweep must still be correct). */
65+
event eSweep: (from: machine, consistent: bool, crashBeforeDelete: bool);
66+
event eSweepDone;
67+
68+
/* Spec events, delivered to monitors via announce. */
69+
event eObjStored: ObjKey;
70+
event eObjReaped: ObjKey;
71+
event eQueueDeleted;
72+
event eSweepQuiesced;

‎p/delete-stream-anchor/PSrc/GC.p‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
/* The GC sweep / reaper. It lists the prefix and reads the anchor, then reaps the
2+
whole prefix iff objects are present AND the anchor is absent (the "should be
3+
empty" classification). consistent selects the anchor read mode: a consistent
4+
read sees the committed anchor, a local read can see a stale cache.
5+
crashBeforeDelete drops the reap to model a crash after the decision; because
6+
the anchor's absence is permanent, a later sweep is still correct. */
7+
machine GC {
8+
var s3: machine;
9+
var khepri: machine;
10+
11+
start state Serving {
12+
entry (init: (s3: machine, khepri: machine)) {
13+
s3 = init.s3;
14+
khepri = init.khepri;
15+
}
16+
on eSweep do (p: (from: machine, consistent: bool, crashBeforeDelete: bool)) {
17+
var n: int;
18+
var anchorPresent: bool;
19+
send s3, eS3List, (from = this,);
20+
receive { case eS3ListResult: (c: int) { n = c; } }
21+
send khepri, eReadAnchor, (from = this, consistent = p.consistent);
22+
receive { case eAnchorResult: (b: bool) { anchorPresent = b; } }
23+
if (n > 0 && !anchorPresent && !p.crashBeforeDelete) {
24+
send s3, eS3DeleteAll, (from = this,);
25+
receive { case eS3Ack: { } }
26+
}
27+
send p.from, eSweepDone;
28+
}
29+
}
30+
}

‎p/delete-stream-anchor/PSrc/Khepri.p‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
/* Khepri: the committed truth plus a lagging local replica cache.
2+
3+
committedAnchor / committedQueue are the durable, quorum-agreed state. A write
4+
updates the committed state immediately but does NOT update the local cache;
5+
eReplicate models the replica catching up. A consistent read returns the
6+
committed anchor (what a quorum read sees); a local read returns the cached
7+
anchor, which can lag.
8+
9+
The anchor is keep_while'd to the queue: deleting the queue removes the anchor
10+
in the SAME committed transaction, which is why "anchor absent" is produced
11+
atomically with deletion and is permanent. */
12+
machine Khepri {
13+
var committedQueue: bool;
14+
var committedAnchor: bool;
15+
var cachedAnchor: bool;
16+
17+
start state Serving {
18+
entry {
19+
committedQueue = true;
20+
committedAnchor = false;
21+
cachedAnchor = false;
22+
}
23+
24+
on eWriteAnchor do (p: (from: machine)) {
25+
/* The anchor exists only while the queue does (keep_while). The local cache
26+
is intentionally NOT updated here, so a local read lags until eReplicate. */
27+
if (committedQueue) {
28+
committedAnchor = true;
29+
}
30+
send p.from, eKAck;
31+
}
32+
33+
on eReplicate do (p: (from: machine)) {
34+
cachedAnchor = committedAnchor;
35+
send p.from, eKAck;
36+
}
37+
38+
on eDeleteQueue do (p: (from: machine)) {
39+
/* keep_while removes the anchor in the same transaction as the queue. */
40+
committedQueue = false;
41+
committedAnchor = false;
42+
announce eQueueDeleted;
43+
send p.from, eKAck;
44+
}
45+
46+
on eReadAnchor do (p: (from: machine, consistent: bool)) {
47+
var present: bool;
48+
if (p.consistent) {
49+
present = committedAnchor;
50+
} else {
51+
present = cachedAnchor;
52+
}
53+
send p.from, eAnchorResult, present;
54+
}
55+
}
56+
}

‎p/delete-stream-anchor/PSrc/S3Store.p‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
/* The S3 object store for the stream's prefix. A LIST returns the current object
2+
count; a reap deletes the whole prefix. Each store and each delete is announced
3+
so the monitors can tell a live-stream reap from a legitimate junk reap. */
4+
machine S3Store {
5+
var objects: map[ObjKey, bool];
6+
7+
start state Serving {
8+
on eS3Put do (p: (from: machine, key: ObjKey)) {
9+
if (!(p.key in objects)) {
10+
objects += (p.key, true);
11+
}
12+
announce eObjStored, p.key;
13+
send p.from, eS3Ack;
14+
}
15+
on eS3DeleteAll do (p: (from: machine)) {
16+
var ks: seq[ObjKey];
17+
var i: int;
18+
ks = keys(objects);
19+
i = 0;
20+
while (i < sizeof(ks)) {
21+
announce eObjReaped, ks[i];
22+
i = i + 1;
23+
}
24+
objects = default(map[ObjKey, bool]);
25+
send p.from, eS3Ack;
26+
}
27+
on eS3List do (p: (from: machine)) {
28+
send p.from, eS3ListResult, sizeof(objects);
29+
}
30+
}
31+
}

‎p/delete-stream-anchor/PSrc/Writer.p‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
/* The writer / replica reader. Before the first fragment it ensures the anchor is
2+
committed, then PUTs the fragment. anchorBeforeFragment honors the load-bearing
3+
ordering; with it false the writer PUTs first and writes the anchor late, which
4+
the ordering-violation test uses to expose a live-stream reap. */
5+
machine Writer {
6+
var s3: machine;
7+
var khepri: machine;
8+
9+
start state Idle {
10+
entry (init: (s3: machine, khepri: machine)) {
11+
s3 = init.s3;
12+
khepri = init.khepri;
13+
}
14+
on eEnsureAnchorThenPut do (p: (from: machine, key: ObjKey, anchorBeforeFragment: bool)) {
15+
if (p.anchorBeforeFragment) {
16+
send khepri, eWriteAnchor, (from = this,);
17+
receive { case eKAck: { } }
18+
send s3, eS3Put, (from = this, key = p.key);
19+
receive { case eS3Ack: { } }
20+
} else {
21+
send s3, eS3Put, (from = this, key = p.key);
22+
receive { case eS3Ack: { } }
23+
send khepri, eWriteAnchor, (from = this,);
24+
receive { case eKAck: { } }
25+
}
26+
send p.from, eWriterDone;
27+
}
28+
}
29+
}

0 commit comments

Comments
 (0)