Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 56 additions & 0 deletions tests/canonical_append_log.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
//! Canonical example: Append-only log with crash-consistency verification.
//!
//! This test validates the FIRST API by performing a simple append-log
//! workload with explicit crash points and invariant checking.

use std::fs::File;
use std::io::{Read, Write};

#[test]
fn append_log_atomicity() {
first::test()
.run(|env| {
let path = env.path("append.log");

// Write record 1
let mut file = File::create(&path).unwrap();
file.write_all(b"RECORD1\n").unwrap();
first::crash_point("after_write_1");

// Write record 2
file.write_all(b"RECORD2\n").unwrap();
first::crash_point("after_write_2");

// Fsync to make durable
file.sync_all().unwrap();
first::crash_point("after_fsync");
})
.verify(|env, crash_info| {
let path = env.path("append.log");

// Read whatever survived
let mut contents = String::new();
if let Ok(mut f) = File::open(&path) {
f.read_to_string(&mut contents).ok();
}

let records: Vec<_> = contents.lines().collect();

// INVARIANT: Records are prefix-consistent
// Either: [], ["RECORD1"], or ["RECORD1", "RECORD2"]
// Never: ["RECORD2"] alone (would violate append-only semantics)

match records.as_slice() {
[] => { /* Nothing persisted - fine */ }
["RECORD1"] => { /* Partial - fine */ }
["RECORD1", "RECORD2"] => { /* Complete - fine */ }
Comment on lines +39 to +46

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Enforce durability after fsync crash point

The invariant currently allows [] or "RECORD1" even when the crash happens at the explicit after_fsync point. At that point fsync() has returned, so the log should be fully durable under FIRST’s model; accepting empty/partial states will let durability regressions (e.g., missing/ignored fsync) pass undetected. Consider using crash_info.label (or point id) to require "RECORD1","RECORD2" when the crash is at after_fsync.

Useful? React with 👍 / 👎.

other => {
panic!(
"Invariant violation at '{}': unexpected log state {:?}",
crash_info.label, other
);
}
}
})
.execute();
}