Explicit state-space exploration is memory-bound: the reachability graph holds every marking it has seen, and the search needs all of them at once to recognise a marking it has already visited. These numbers say how much that costs.
Reproduce with:
mix run bench/reachability.exs 11 13 # the dining-philosopher rows below
mix run bench/million.exs # the million-marking rows below
mix run bench/reachability.exs # the default sizes 5, 7 and 9
A run stopped by its limit is labelled PARTIAL and is not a measurement of
a state space; every row below is a complete exploration.
Memory is the peak total the VM reports (processes and ETS together) while the exploration runs, sampled every millisecond, minus the reading taken before it starts. Measuring after the fact would miss the peak, because the visited set is released as soon as the graph is built. Peak therefore includes garbage not yet collected, which is part of what an exploration really needs — and also what makes it the one figure here that moves between runs, by up to a fifth. Ranges below are the spread over three runs; everything else was stable to the digits shown.
Measured on Elixir 1.19.5, OTP 28, aarch64-apple-darwin (Apple Silicon). Figures below 10,000 markings are dominated by noise and are not reported.
Reachability
| net | places | markings | edges | time | markings/s | bytes/marking | peak |
|---|---|---|---|---|---|---|---|
| dining philosophers 11, map | 44 | 16,238 | 115,467 | 0.06 s | 293,000 | 2,188 | 33 MiB |
| dining philosophers 11, ETS | 44 | 16,238 | 115,467 | 0.06 s | 261,000 | 3,332 | 51 MiB |
| dining philosophers 13, map | 52 | 94,642 | 795,353 | 0.49 s | 194,000 | 2,903 | 262–277 MiB |
| dining philosophers 13, ETS | 52 | 94,642 | 795,353 | 0.50 s | 190,000 | 2,443 | 220 MiB |
| dining philosophers 13, map, no edges | 52 | 94,642 | 795,353 | 0.42 s | 228,000 | 2,139 | 193 MiB |
| dining philosophers 15, map, no edges | 60 | 551,614 | 5,348,835 | 3.57 s | 154,000 | 1,890–2,268 | 994–1,193 MiB |
| producer-consumer, buffer 250,000, map | 6 | 1,000,004 | 2,000,004 | 1.32 s | 760,000 | 724 | 690 MiB |
| producer-consumer, buffer 250,000, ETS | 6 | 1,000,004 | 2,000,004 | 1.13 s | 887,000 | 598 | 570 MiB |
| producer-consumer, buffer 250,000, map, no edges | 6 | 1,000,004 | 2,000,004 | 1.00 s | 997,000 | 339–376 | 324–359 MiB |
The producer-consumer with buffer 100 (404 markings) runs in under a millisecond; it is in the benchmark script because it is a standard shape, not because the number means anything.
What the numbers say
A million markings fits in a gigabyte, if the net is narrow. The producer-consumer with a buffer of 250,000 has 1,000,004 reachable markings and 2,000,004 edges, explored in 690 MiB with the edge list and about 350 MiB without it, at 0.8 to 1.0 million markings per second. Both are within the 1 GB target.
Bytes per marking follow the number of places. A marking is a tuple of counts, one machine word each plus a header: 56 bytes for the 6-place producer-consumer and 424 bytes for the 52-place dining philosophers at 13. The rest of the 724 and 2,903 bytes measured is the edge list, the visited set mapping each marking to its state number, and garbage not yet collected. Packing a marking into a binary would attack the first of those three, which is the largest for a wide net and the smallest for a narrow one.
The dining philosophers at 15 need 1.0 to 1.2 GiB for 551,614 markings, so a million markings of that shape would need somewhere between 1.8 and 2.2 GB: the target is met per marking, not per net. A net wide enough to matter is usually also one whose state space grows too fast to enumerate anyway.
Edges are a quarter to a half of the cost. Dropping them
(edges: false) saves 26% of the peak on the 13 philosophers and 49% on the
million-marking producer-consumer — the wider the net, the more of the cost
is markings rather than edges — and a little time with it. bound/3, deadlocks/3 and
dead_transitions/3 already do this; only callers that want the graph
itself pay for it.
Map and ETS are close. The ETS visited set is faster and smaller at a
million markings (1.13 s and 570 MiB against 1.32 s and 690 MiB) and worse
below about 100,000, where the map stays in the process heap and copying
into ETS does not pay off — at 16,238 markings ETS peaks at 51 MiB against
the map's 33 MiB. The default is :map
because it wins on the sizes most nets reach; store: :ets is worth setting
for the large ones.
What would move these numbers
Not in version 1.0, and listed here so the measurements have a direction:
- Packing markings. Counts are stored as a tuple of integers, one word each. Bit-packing a marking into a binary, sized by the bound of each place, would cut bytes per marking several-fold for wide nets.
- Partial-order reduction. Stubborn sets explore a fraction of the interleavings while preserving deadlocks and boundedness. This is the change that moves a state space from millions to thousands, and it is explicitly out of scope for 1.0.
- Not storing markings twice. A marking is currently referenced by both the visited set and the graph. They share the same term, so the cost is one word per marking, but a compact representation would make the difference larger.