prismulti 0.1.1

A multi-threaded Rust implementation of a subset of the PRISM model checker.
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

# DD Manager Usage Notes

This document explains how to use `src/dd_manager/`, with emphasis on
`protected_local` and `protected_slot`.

## Why protection exists

Sylvan uses garbage collection with a mark-and-sweep style reachability pass.
In practice, nodes that are reachable from protected roots are kept alive, and
unreachable nodes may be reclaimed during GC.

`Sylvan_mtbdd_protect(ptr)` registers a pointer to an `MTBDD` slot as a root.
`Sylvan_mtbdd_unprotect(ptr)` removes that root registration.

If an intermediate/result node is not protected when needed, later DD calls may
trigger GC and reclaim it.

## Two protection mechanisms

### `protected_local` (stack-local, temporary roots)

Source: `src/dd_manager/protected_local.rs`

- `ProtectedLocal` stores an `MTBDD` in a local variable slot.
- `protect()` registers that slot with Sylvan.
- `Drop` calls `unprotect()`.
- Typed wrappers exist for domain types:
  - `ProtectedBddLocal`
  - `ProtectedAddLocal`
  - `ProtectedMapLocal`
  - `ProtectedVarSetLocal`

Important: do not rely on calling `new(...)` alone. Protection must happen only
after the value is in its final local slot. Use the macros:

- `protected_bdd!(name, expr)`
- `protected_add!(name, expr)`
- `protected_map!(name, expr)`
- `protected_var_set!(name, expr)`

Each macro expands to:

```rust
# use prismulti::dd_manager::{dd, protected_local::ProtectedBddLocal, DDManager};
# let mut mgr = DDManager::new();
# let x_idx = mgr.new_var();
# let expr = dd::bdd_var(&mgr, x_idx);
let mut name = ProtectedBddLocal::new(expr);
name.protect();
```

This avoids protecting a pointer before a move of the local binding.

### `protected_slot` (owned, long-lived roots)

Source: `src/dd_manager/protected_slot.rs`

- `ProtectedSlot` stores `MTBDD` inside a `Box<MTBDD>`.
- It protects eagerly in `new(...)` and unprotects in `Drop`.
- Because the value is boxed, the protected pointer stays stable even if the
  wrapper itself is moved.
- Typed wrappers:
  - `ProtectedBddSlot`
  - `ProtectedAddSlot`
  - `ProtectedVarSetSlot`

Use this for fields that must stay rooted across many operations (for example,
roots stored in `SymbolicDTMC`).

## Calling convention in this codebase

This repository follows a strict convention for DD operations:

- The caller is responsible for protecting all argument nodes before calling a
  function.
- The caller is also responsible for protecting the returned node if it must
  survive subsequent DD operations.
- Callees should only protect their own internal temporaries.

In other words: ownership of root-liveness is at call boundaries.

### What this means in practice

- Public functions in `src/dd_manager/dd.rs` mostly pass and return plain
  `BddNode`/`AddNode`/`VarSet` values.
- Those values are not automatically rooted by the function API.
- Functions use `protected_*!` only for internal intermediate values that must
  remain alive while building the final result.

## Example patterns

### Caller-side protection

```rust
# use prismulti::dd_manager::{dd, DDManager};
# use prismulti::protected_bdd;
# let mut mgr = DDManager::new();
# let x_idx = mgr.new_var();
protected_bdd!(x, dd::bdd_var(&mgr, x_idx));
protected_bdd!(not_x, dd::bdd_not(x.get()));

let combined = dd::bdd_and(x.get(), not_x.get());
protected_bdd!(combined_root, combined);
# let _ = combined_root.get();
```

### Callee-side temporaries only

```rust
# use prismulti::dd_manager::{dd, AddNode, BddNode};
# use prismulti::protected_bdd;
pub fn add_equals(a: AddNode, b: AddNode) -> BddNode {
    protected_bdd!(gt, dd::add_greater_than(a, b));
    protected_bdd!(lt, dd::add_less_than(a, b));
    protected_bdd!(neq, dd::bdd_or(gt.get(), lt.get()));
    dd::bdd_not(neq.get())
}
```

The callee protects only `gt`, `lt`, `neq` (its internal temporaries). The
caller must root the returned value if needed beyond immediate use.

## Rule of thumb

- Use `protected_local` macros for short-lived locals in expression-building
  code.
- In iterative/hot loops, predeclare reusable `protected_local` slots before the
  loop and update them with `.replace(...)`/`.set(...)` each iteration, instead
  of creating new protected locals inside the loop body.
- Use `protected_slot` for long-lived owned roots in structs.
- Never assume a plain returned node stays alive unless you root it on the
  caller side.
- Never assume that temporaries between DD calls stay alive unless you protect them by storing the intermediate result in a `protected_local` or `protected_slot`.