|
| 1 | +//! Canonical example: Append-only log with crash-consistency verification. |
| 2 | +//! |
| 3 | +//! This test validates the FIRST API by performing a simple append-log |
| 4 | +//! workload with explicit crash points and invariant checking. |
| 5 | +
|
| 6 | +use std::fs::File; |
| 7 | +use std::io::{Read, Write}; |
| 8 | + |
| 9 | +#[test] |
| 10 | +fn append_log_atomicity() { |
| 11 | + first::test() |
| 12 | + .run(|env| { |
| 13 | + let path = env.path("append.log"); |
| 14 | + |
| 15 | + // Write record 1 |
| 16 | + let mut file = File::create(&path).unwrap(); |
| 17 | + file.write_all(b"RECORD1\n").unwrap(); |
| 18 | + first::crash_point("after_write_1"); |
| 19 | + |
| 20 | + // Write record 2 |
| 21 | + file.write_all(b"RECORD2\n").unwrap(); |
| 22 | + first::crash_point("after_write_2"); |
| 23 | + |
| 24 | + // Fsync to make durable |
| 25 | + file.sync_all().unwrap(); |
| 26 | + first::crash_point("after_fsync"); |
| 27 | + }) |
| 28 | + .verify(|env, crash_info| { |
| 29 | + let path = env.path("append.log"); |
| 30 | + |
| 31 | + // Read whatever survived |
| 32 | + let mut contents = String::new(); |
| 33 | + if let Ok(mut f) = File::open(&path) { |
| 34 | + f.read_to_string(&mut contents).ok(); |
| 35 | + } |
| 36 | + |
| 37 | + let records: Vec<_> = contents.lines().collect(); |
| 38 | + |
| 39 | + // INVARIANT: Records are prefix-consistent |
| 40 | + // Either: [], ["RECORD1"], or ["RECORD1", "RECORD2"] |
| 41 | + // Never: ["RECORD2"] alone (would violate append-only semantics) |
| 42 | + |
| 43 | + match records.as_slice() { |
| 44 | + [] => { /* Nothing persisted - fine */ } |
| 45 | + ["RECORD1"] => { /* Partial - fine */ } |
| 46 | + ["RECORD1", "RECORD2"] => { /* Complete - fine */ } |
| 47 | + other => { |
| 48 | + panic!( |
| 49 | + "Invariant violation at '{}': unexpected log state {:?}", |
| 50 | + crash_info.label, other |
| 51 | + ); |
| 52 | + } |
| 53 | + } |
| 54 | + }) |
| 55 | + .execute(); |
| 56 | +} |
0 commit comments