1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
//! Differential property test for the Phase 9 per-thread heap (`alloc`
//! feature). Models `Heap` against a reference (a `Vec` of live allocations).
//! Encodes invariants M1--M4 through the heap layer.
//!
//! Per the short-scenario policy: ~64 cases, small sizes.
#![cfg(feature = "alloc")]
use std::alloc::Layout;
use proptest::prelude::*;
use sefer_alloc::Heap;
/// A live allocation in the model.
#[derive(Clone)]
struct Live {
ptr: *mut u8,
size: usize,
align: usize,
}
unsafe impl Send for Live {}
/// Operations applied to both the model and `Heap`.
#[derive(Clone, Debug)]
enum Op {
Alloc { size: usize, align: usize },
Dealloc(usize),
Realloc { i: usize, new_size: usize },
AllocZeroed { size: usize, align: usize },
}
fn small_size() -> impl Strategy<Value = usize> {
// Mostly small (the hot free-list path); occasionally large (> SMALL_MAX,
// the dedicated-segment path). The large arm is weighted rare and capped at
// 128 KiB — enough to exercise the large path (SMALL_MAX is ~94 KiB) while
// keeping the suite fast per the short-scenario policy (no multi-MiB
// byte-by-byte writes).
prop_oneof![
9 => (1usize..=4096).prop_map(|s| s.max(1)),
1 => (4097usize..=128 * 1024).prop_map(|s| s.max(1)),
]
}
fn small_align() -> impl Strategy<Value = usize> {
prop_oneof![
Just(1usize),
Just(2usize),
Just(4usize),
Just(8usize),
Just(16usize),
Just(4096usize),
]
}
fn ranges_overlap(a: usize, asize: usize, b: usize, bsize: usize) -> bool {
!(a + asize <= b || b + bsize <= a)
}
proptest! {
// `failure_persistence: None` — do not write a regressions file (avoids the
// "SourceParallel failed to find lib.rs" abort under some run layouts and
// keeps runs hermetic), matching the Phase 7d / Phase 8 differential tests.
#![proptest_config(ProptestConfig { cases: 64, failure_persistence: None, ..ProptestConfig::default() })]
#[test]
fn heap_matches_reference_model(
ops in prop::collection::vec(
prop_oneof![
(small_size(), small_align()).prop_map(|(s, a)| Op::Alloc { size: s, align: a }),
any::<usize>().prop_map(Op::Dealloc),
(any::<usize>(), small_size()).prop_map(|(i, ns)| Op::Realloc { i, new_size: ns }),
(small_size(), small_align()).prop_map(|(s, a)| Op::AllocZeroed { size: s, align: a }),
],
0..200,
)
) {
let mut heap = Heap::new().expect("heap bootstrap");
let mut live: Vec<Live> = Vec::new();
for op in ops {
match op {
Op::Alloc { size, align } => {
let layout = Layout::from_size_align(size, align).unwrap();
let ptr = heap.alloc(layout);
prop_assert!(!ptr.is_null(), "alloc returned null");
prop_assert_eq!(
(ptr as usize) % align, 0,
"pointer not aligned"
);
// M3: no overlap with any live allocation.
for other in live.iter() {
prop_assert!(
!ranges_overlap(ptr as usize, size, other.ptr as usize, other.size),
"new alloc overlaps live"
);
}
// Write pattern + read back (M1 validity).
unsafe {
for b in 0..size {
ptr.add(b).write(0xA7);
}
for b in 0..size {
prop_assert_eq!(ptr.add(b).read(), 0xA7, "byte did not read back");
}
}
live.push(Live { ptr, size, align });
}
Op::AllocZeroed { size, align } => {
let layout = Layout::from_size_align(size, align).unwrap();
let ptr = heap.alloc_zeroed(layout);
prop_assert!(!ptr.is_null());
prop_assert_eq!((ptr as usize) % align, 0);
unsafe {
for b in 0..size {
prop_assert_eq!(ptr.add(b).read(), 0, "byte not zeroed");
}
}
live.push(Live { ptr, size, align });
}
Op::Dealloc(i) => {
if !live.is_empty() {
let i = i % live.len();
let l = live.swap_remove(i);
heap.dealloc(l.ptr, Layout::from_size_align(l.size, l.align).unwrap());
}
}
Op::Realloc { i, new_size } => {
if !live.is_empty() {
let i = i % live.len();
let l = live[i].clone();
let old_layout = Layout::from_size_align(l.size, l.align).unwrap();
let new_ptr = heap.realloc(l.ptr, old_layout, new_size);
if !new_ptr.is_null() {
prop_assert_eq!((new_ptr as usize) % l.align, 0);
// M1/realloc: the preserved prefix (the `min(old,new)`
// bytes) must equal what was written before. NOTE: a
// GROWN realloc leaves the tail `[old..new)`
// UNINITIALISED — that is correct allocator behaviour
// (realloc does not zero the grown region). When the
// new block is reused from the free list, that tail
// holds stale bytes, NOT zero. So we (a) check only the
// preserved prefix here, then (b) re-establish the
// pattern over the FULL new size so a later realloc of
// this entry checks against known contents (not the
// uninitialised tail). Phase 8's substrate test passed
// this check only vacuously, because fresh OS pages are
// zeroed; the heap's free-list reuse exposes the real
// (correct) semantics.
let keep = l.size.min(new_size);
unsafe {
for b in 0..keep {
let v = new_ptr.add(b).read();
prop_assert!(
v == 0xA7 || v == 0,
"realloc did not preserve the prefix"
);
}
for b in 0..new_size {
new_ptr.add(b).write(0xA7);
}
}
live[i] = Live { ptr: new_ptr, size: new_size, align: l.align };
}
}
}
}
}
// Free all survivors.
for l in &live {
heap.dealloc(l.ptr, Layout::from_size_align(l.size, l.align).unwrap());
}
drop(live);
drop(heap);
}
}