lib/reducer/src/bytes/storage.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! `Storage` holds the backing memory a byte reduction run needs, allocated
2 //! once up front and reused for every run: the *workspace*. The `alloc_phase`
3 //! checker tracks the phase and establishes that the owner makes no further
4 //! backing allocation once the workspace is activated into steady state.
5 //!
6 //! ## Workspace Lifecycle
7 //!
8 //! | Operation | Effect / Transition |
9 //! | :--- | :--- |
10 //! | `storage.activate()` | Moves `initialization` to `steady (idle)` |
11 //! | `storage.acquire(bytes)` | Leases `steady (idle)` to `steady (acquired)` |
12 //! | `result.deinit()` / `storage.release()` | Releases `steady (acquired)` back to `steady (idle)` |
13 //! | `storage.deinit(allocator)` (unactivated) | Frees unactivated `initialization` to `teardown` |
14 //! | `storage.deinit(allocator)` (idle) | Frees idle `steady` to `teardown` (invalid while acquired) |
15 //!
16 //! 1. **Initialization (`Phase.initialization`)**: `Storage.init()` derives the
17 //! layout, which comes to $N + \max(N - 1, 0)$ bytes (its *capacity*), and
18 //! allocates the backing buffer once. The instance starts out with
19 //! `phase = .initialization`. A workspace that is never activated can be
20 //! freed straight away by `storage.deinit(allocator)`, using the allocator
21 //! `init()` received. Filling in `Storage` fields by hand is unsafe, so
22 //! callers reach a valid workspace through `init()`.
23 //! 2. **Activation (`Phase.steady`)**: the caller calls `storage.activate()`,
24 //! which seals the initialization phase and moves the workspace to steady
25 //! and idle. In steady state the workspace owner allocates nothing further.
26 //! 3. **Acquisition (`in_use = true`)**: inside `reduce()`,
27 //! `storage.acquire(input_bytes)` checks that the workspace is in steady
28 //! phase, checks that no lease is out, and checks that `input_bytes` is
29 //! within `max_input_bytes`. It sets `in_use = true` and returns the two
30 //! byte lanes as `Regions`, returning slices, copying nothing into the
31 //! witness lane and initializing nothing. An oversized input returns
32 //! `error.InputCapacityExceeded`, and a request made while a lease is out
33 //! returns `error.ReductionStorageInUse`, both before any workspace byte
34 //! changes.
35 //! 4. **Release and reuse (`in_use = false`)**: when a run finishes,
36 //! `Result.deinit()`, or `storage.release()`, clears `in_use`. The workspace
37 //! returns to steady and idle, and a later run can acquire it with no
38 //! further allocation.
39 //! 5. **Teardown (`Phase.teardown`)**: `storage.deinit(allocator)` checks that
40 //! no lease is out, sets `phase = .teardown`, and frees the backing buffer
41 //! with the same allocator `init()` received.
42 //!
43 //! ## Ownership and Concurrency Constraints
44 //! - `Storage` offers no thread safety. `in_use` is a plain boolean that turns
45 //! away a second use on one thread, so reaching one workspace from multiple
46 //! threads at once is the caller's to synchronize.
47 //! - Zig checks no linear or affine type at compile time, and a runtime check
48 //! catches no shallow copy of a `Storage` or a `Result`, so one owner holds
49 //! each of them, makes no shallow duplicate, and leaves the bookkeeping
50 //! fields alone.
51 //! - The capacity claim `reducer.byte_storage` covers the two internal byte
52 //! lanes. It leaves out the caller's own initial input bytes, the predicate's
53 //! context, and every allocation and foreign side effect the callback
54 //! performs.
55
56 const std = @import("std");
57 const alloc_phase = @import("alloc_phase");
58 const capacity_mod = @import("capacity.zig");
59 const model = @import("model.zig");
60
61 /// Pair of memory lane slices `Storage.acquire()` returns. `acquire()` copies
62 /// nothing into these slices and initializes nothing in them: they are
63 /// sub-slices of the backing allocation.
64 pub const Regions = struct {
65 /// Slice of the witness lane sized to this run's `input_bytes`.
66 current: []u8,
67
68 /// Scratch lane, whose length is `candidate_bytes`, which is
69 /// $\max(N - 1, 0)$.
70 candidate: []u8,
71 };
72
73 /// Snapshot of one workspace's state, taken by value at the moment of the call.
74 pub const Status = struct {
75 /// Workspace current phase, one of `.initialization`, `.steady`, or
76 /// `.teardown`.
77 phase: alloc_phase.capacity.Phase,
78
79 /// Flag recording whether a running reduction or a `Result` whose
80 /// `deinit()` has yet to be called currently holds the workspace.
81 in_use: bool,
82
83 /// Derived capacity the workspace was configured for, which is
84 /// $N + \max(N - 1, 0)$ bytes. The figure is a record of the configured
85 /// size, and it stays recorded after teardown.
86 storage_bytes: usize,
87
88 /// Longest input in bytes this workspace serves, which is $N$.
89 max_input_bytes: usize,
90 };
91
92 /// Workspace, allocated up front and double-buffered, that carries reduction in
93 /// steady state. It holds the backing allocation and tracks the phase it is in
94 /// and whether a lease is out.
95 pub const Storage = struct {
96 /// Lifecycle phase that `alloc_phase` enforces.
97 phase: alloc_phase.capacity.Phase,
98
99 /// Layout derived while initializing.
100 capacity: capacity_mod.Capacity,
101
102 /// Entire contiguous backing byte allocation.
103 bytes: []u8,
104
105 /// Fixed sub-slice reserved for the witness lane, spanning $0 \dots N$.
106 current: []u8,
107
108 /// Fixed sub-slice reserved for the scratch lane, spanning
109 /// $N \dots N + \max(N - 1, 0)$.
110 candidate: []u8,
111
112 /// Flag recording that a lease is out, turning away a reentrant acquisition
113 /// and one made while an earlier result is still live.
114 in_use: bool = false,
115
116 /// Re-export of the capacity limits type.
117 pub const Limits: type = capacity_mod.Limits;
118
119 /// Re-export of the derived capacity type.
120 pub const Capacity: type = capacity_mod.Capacity;
121
122 /// Re-export of the exhaustion error set.
123 pub const Exhaustion: type = model.Exhaustion;
124
125 /// Errors `Storage.init()` may return.
126 pub const InitError = std.mem.Allocator.Error || capacity_mod.DeriveError;
127
128 /// Stardust capacity declaration that phase-directed allocation
129 /// verification reads. It records that the workspace owner makes no further
130 /// backing allocation once sealed into steady state. It bounds the storage
131 /// by $2 \times \text{max\_input\_bytes}$. It leaves out the memory and the
132 /// effects the caller's predicate owns.
133 pub const claim: alloc_phase.capacity.Declaration = .{
134 .source = .{
135 .id = "reducer.byte_storage",
136 .kind = .phase_static,
137 .limit_source = .caller,
138 .storage = .{
139 .covered = &.{
140 .{
141 .id = "accepted_input_and_borrowed_result_bytes",
142 .lifetime = .steady,
143 .detail = "accepted input and borrowed result bytes",
144 },
145 .{
146 .id = "deletion_candidate_scratch_bytes",
147 .lifetime = .steady,
148 .detail = "deletion candidate scratch bytes",
149 },
150 },
151 .excluded = &.{
152 "caller-owned initial input bytes",
153 "caller-owned predicate context, allocation, and effects",
154 },
155 },
156 .capacity = .{
157 .inputs = &.{
158 alloc_phase.capacity.bindInput(Limits, "max_input_bytes", "max_input_bytes"),
159 },
160 .type_selectors = &.{},
161 .nodes = &.{
162 .{ .input = 0 },
163 .{ .scale = .{ .node = 0, .coefficient = .{ .literal = 2 } } },
164 },
165 .assertions = &.{.{
166 .scope = .closure_total,
167 .measure = .retained,
168 .relation = .upper_bound,
169 .expression = 1,
170 }},
171 },
172 .overload = .{
173 .kind = .reject_before_mutation,
174 .detail = "oversize and concurrent requests fail before workspace bytes change",
175 },
176 .risks = .{
177 .transitive = .{
178 .status = .witnessed,
179 .detail = "reduction uses byte lanes; predicate effects remain caller-owned",
180 },
181 .foreign = .{
182 .status = .excluded,
183 .detail = "predicate and operating-system effects are caller-owned",
184 },
185 },
186 .obligations = &.{
187 .{ .key = "reducer_byte_capacity", .role = .capacity_model },
188 .{ .key = "reducer_byte_acquisition", .role = .custom },
189 .{ .key = "reducer_byte_oom", .role = .custom },
190 .{ .key = "reducer_byte_boundaries", .role = .overload },
191 .{ .key = "reducer_byte_reuse", .role = .overload },
192 .{ .key = "reducer_byte_sealed", .role = .transitive_risk },
193 .{ .key = "reducer_byte_callback", .role = .foreign_risk },
194 .{ .key = "reducer_byte_root", .role = .custom },
195 },
196 },
197 .bindings = .{
198 .owner = @This(),
199 .seal = .{
200 .family = alloc_phase.capacity.selector(@This().activate),
201 .premise = .{
202 .class = .checked_semantic_fact,
203 .authority = .checker,
204 },
205 },
206 .teardown = .{
207 .family = alloc_phase.capacity.selector(@This().deinit),
208 .premise = .{
209 .class = .checked_semantic_fact,
210 .authority = .checker,
211 },
212 },
213 },
214 };
215
216 /// Allocates a reduction workspace and divides it into the two lanes, sized
217 /// for inputs up to `limits.max_input_bytes`. The new workspace is in
218 /// `.initialization`, and the caller calls `storage.activate()` on it
219 /// before passing it to `reduce()`. A workspace that is never activated can
220 /// be freed directly by `storage.deinit()`.
221 ///
222 /// ## Errors
223 /// - `error.CapacityOverflow` when $N + \max(N - 1, 0)$ overflows `usize`.
224 /// - `error.OutOfMemory` when the allocator declines the request.
225 pub fn init(allocator: std.mem.Allocator, limits: Limits) InitError!Storage {
226 const capacity = try Capacity.derive(limits);
227 const bytes = try allocator.alloc(u8, capacity.storage_bytes);
228 const owner = Storage{
229 .phase = .initialization,
230 .capacity = capacity,
231 .bytes = bytes,
232 .current = bytes[0..limits.max_input_bytes],
233 .candidate = bytes[capacity.candidate_offset..][0..capacity.candidate_bytes],
234 };
235 std.debug.assert(owner.current.len == limits.max_input_bytes);
236 std.debug.assert(owner.candidate.len == capacity.candidate_bytes);
237 std.debug.assert(owner.current.len + owner.candidate.len == owner.bytes.len);
238 return owner;
239 }
240
241 /// Moves the workspace from `.initialization` to `.steady`. Once it
242 /// returns, the workspace owner makes no further heap allocation.
243 ///
244 /// ## Preconditions
245 /// - `self.phase` is `.initialization`.
246 /// - The backing allocation's length equals `self.capacity.storage_bytes`.
247 pub fn activate(self: *Storage) void {
248 std.debug.assert(self.phase == .initialization);
249 std.debug.assert(self.bytes.len == self.capacity.storage_bytes);
250 self.phase = .steady;
251 }
252
253 /// Takes exclusive use of the workspace for a run over `input_bytes` bytes.
254 /// It returns `Regions` holding sub-slices of the backing buffer. It copies
255 /// nothing into `Regions.current`.
256 ///
257 /// ## Preconditions
258 /// - `self.phase` is `.steady`.
259 ///
260 /// ## Errors
261 /// - `error.ReductionStorageInUse` when `self.in_use` is already true. A
262 /// reentrant call, and a call made while an earlier result is still live,
263 /// are both turned away without disturbing the hold that is already out.
264 /// - `error.InputCapacityExceeded` when `input_bytes` exceeds
265 /// `max_input_bytes`.
266 pub fn acquire(self: *Storage, input_bytes: usize) Exhaustion!Regions {
267 std.debug.assert(self.phase == .steady);
268 if (self.in_use) return error.ReductionStorageInUse;
269 if (input_bytes > self.capacity.limits.max_input_bytes) {
270 return error.InputCapacityExceeded;
271 }
272 std.debug.assert(self.current.len == self.capacity.limits.max_input_bytes);
273 std.debug.assert(self.candidate.len == self.capacity.candidate_bytes);
274 self.in_use = true;
275 return .{
276 .current = self.current[0..input_bytes],
277 .candidate = self.candidate,
278 };
279 }
280
281 /// Gives up this run's lease, returning the workspace to steady and idle so
282 /// it can serve another run. `Result.deinit()` calls it, and it moves the
283 /// workspace no closer to teardown.
284 ///
285 /// ## Preconditions
286 /// - `self.phase` is `.steady`.
287 /// - `self.in_use` is true.
288 pub fn release(self: *Storage) void {
289 std.debug.assert(self.phase == .steady);
290 std.debug.assert(self.in_use);
291 self.in_use = false;
292 std.debug.assert(!self.in_use);
293 }
294
295 /// Returns a snapshot of this workspace, taken by value at the moment of
296 /// the call.
297 pub fn status(self: *const Storage) Status {
298 return .{
299 .phase = self.phase,
300 .in_use = self.in_use,
301 .storage_bytes = self.capacity.storage_bytes,
302 .max_input_bytes = self.capacity.limits.max_input_bytes,
303 };
304 }
305
306 /// Frees the backing allocation and moves the workspace to `.teardown`. It
307 /// works on an idle steady workspace and on one still in `.initialization`
308 /// that was never activated. It needs the same allocator `Storage.init()`
309 /// received.
310 ///
311 /// ## Preconditions
312 /// - `self.phase` is anything other than `.teardown`.
313 /// - `self.in_use` is false, so every result has had its `deinit()` called.
314 pub fn deinit(self: *Storage, allocator: std.mem.Allocator) void {
315 std.debug.assert(self.phase != .teardown);
316 std.debug.assert(!self.in_use);
317 std.debug.assert(self.bytes.len == self.capacity.storage_bytes);
318 self.phase = .teardown;
319 allocator.free(self.bytes);
320 self.bytes = &.{};
321 self.current = &.{};
322 self.candidate = &.{};
323 }
324 };
325
326 fn checkInitFailures(allocator: std.mem.Allocator) !void {
327 var storage = try Storage.init(allocator, .{ .max_input_bytes = 9 });
328 storage.deinit(allocator);
329 }
330
331 test "byte reduction storage acquires one exact region" {
332 comptime {
333 @stardustClaim(
334 @import("alloc_phase").capacity.witness(Storage, "reducer_byte_acquisition"),
335 null,
336 null,
337 null,
338 null,
339 null,
340 null,
341 );
342 }
343
344 var counting = std.testing.FailingAllocator.init(std.testing.allocator, .{});
345 const limits = capacity_mod.Limits{ .max_input_bytes = 9 };
346 const capacity = try capacity_mod.Capacity.derive(limits);
347 var storage = try Storage.init(counting.allocator(), limits);
348 defer storage.deinit(counting.allocator());
349
350 try std.testing.expectEqual(@as(usize, 1), counting.alloc_index);
351 try std.testing.expectEqual(capacity.storage_bytes, counting.allocated_bytes);
352 try std.testing.expectEqual(alloc_phase.capacity.Phase.initialization, storage.status().phase);
353 storage.activate();
354 const regions = try storage.acquire(9);
355 defer storage.release();
356 try std.testing.expectEqual(@intFromPtr(storage.bytes.ptr), @intFromPtr(regions.current.ptr));
357 try std.testing.expectEqual(
358 @intFromPtr(storage.bytes.ptr) + capacity.candidate_offset,
359 @intFromPtr(regions.candidate.ptr),
360 );
361 }
362
363 test "byte reduction storage retries after every allocation failure" {
364 comptime {
365 @stardustClaim(
366 @import("alloc_phase").capacity.witness(Storage, "reducer_byte_oom"),
367 null,
368 null,
369 null,
370 null,
371 null,
372 null,
373 );
374 }
375
376 try std.testing.checkAllAllocationFailures(std.testing.allocator, checkInitFailures, .{});
377 }
378
379 comptime {
380 alloc_phase.capacity.requireAllocatorRejectingOwnerShape(Storage);
381 }