# Meeting 2023-11-29
<!-- Leave your topic starting with ### in the relevant sections below -->
## Critical
<!-- bugs, soundness issues, urgent patches/reviews etc. -->
## Status Reports
<!-- You want to report on something you are working on/request reviews.
Or you want to know the status of something someone else is doing -->
## Discussion Questions
<!-- Anything that requires lengthy discussion/more general questions also fit here -->
### Abstraction registry page
* [ ] Disclaimer.
* [ ] Start with asking people to add themselves.
### Safety Standard
Benno: I have been working on this for some time. Hope to have something ready to send to the list soon-ish. But wanted to know if you have any particular recommendation as to what it should contain.
One thing that I wanted to ask you guys is how we want to handle `unsafe` blocks with lots of stuff in them. This example from the list if of course not ok
```rust
unsafe {
let mut index: core::ffi::c_ulong = 0;
let mut entry = bindings::xa_find(
self.xa.get(),
&mut index,
core::ffi::c_ulong::MAX,
bindings::BINDINGS_XA_PRESENT,
);
while !entry.is_null() {
T::from_foreign(entry);
entry = bindings::xa_find_after(
self.xa.get(),
&mut index,
core::ffi::c_ulong::MAX,
bindings::BINDINGS_XA_PRESENT,
);
}
}
```
but this is more of a gray zone:
```rust
let ret = unsafe {
bindings::xa_alloc(
self.xa.get(),
&mut id,
new as *mut _,
bindings::xa_limit { min, max },
bindings::GFP_KERNEL,
)
};
```
Since `get()` is a safe operation and the construction of the `xa_limit` struct as well as the cast are also safe.
I was thinking about making a list of allowed safe operations inside `unsafe` blocks, what do you think?
Gary: The second example looks legit, I don't think further splitting make sense.
Another example:
```rust
// SAFETY: `self.xa` is always valid by the type invariant.
let p = unsafe {
bindings::xa_lock(self.xa.get());
bindings::xa_load(self.xa.get(), index.try_into().ok()?)
};
```
Duplication?
<https://github.com/Darksonn/linux/blob/dca45e6c7848e024709b165a306cdbe88e5b086a/rust/kernel/list.rs#L357-L368>
What about?
<https://github.com/Darksonn/linux/blob/dca45e6c7848e024709b165a306cdbe88e5b086a/rust/kernel/list.rs#L432-L437>
### formally verifying Klint (only if we have time!)
I resumed my work on this and finally got to a resonable theory. But I encountered the following issue:
First some definitions:
Since Rust is way to complex, I settled on this simpler toy language:
```
datatype
com = SKIP
| SLEEP
| LOCK var
| UNLOCK var
| Inc var
| Dec var
| CALL var
| Seq com com
| While var a com
```
Here is the operational semantics:
```
inductive small_step :: "'a com × state ⇒ 'a com × state ⇒ bool" (infix "→" 55)
where
Seq1: "(SKIP;;c, s) → (c, s)"
| Call: "(CALL f, s) → (funcs f, s)"
| Sleep: "can_sleep s ⟹ (SLEEP, s) → (SKIP, s)"
| Lock: "unlocked s x ⟹ (LOCK x, s) → (SKIP, lock s x)"
| Unlock: "locked s x ⟹ (UNLOCK x, s) → (SKIP, unlock s x)"
| Inc: "(x++, s) → (SKIP, inc s x)"
| Dec: "(x--, s) → (SKIP, dec s x)"
| Seq2: "(c, s) → (c', s') ⟹ (c;;d, s) → (c';;d, s')"
| WhileTrue: "val s x ≠ 0 ⟹ (WHILE x ≠ 0 DO c, s) → (c;; WHILE x ≠ 0 DO c, s)"
| WhileFalse: "val s x = 0 ⟹ (WHILE x ≠ 0 DO c, s) → (SKIP, s)"
```
I defined soundness like this:
```
definition sound :: "'a com ⇒ bool"
where "⊨ c ≡ ∃l. ∀v. (∃s. (c, (l, v)) →* (SKIP, s))
∨ (∃π. is_exec π ∧ π 0 = (c, (l, v)))"
```
Which in normal language reads:
```!
A program `c` is considered sound, if there exists some set of locked variables `l` such that for every possible assignment of values to variables `v` the program `c` can terminate or run for ever when starting with the state `(l, v)`.
```
To model what klint does I have defined a "typing": each command is given a "type" -- which is just a tuple of the adjustment and the expected range.
```
(a, (s, e)) ⊢ c
```
where `a` is the adjustment, and `[s, e]` is the interval (both s and e are inclusive).
Here is the definition of the typing:
```
inductive typing :: "ty ⇒ 'a com ⇒ bool" (infix "⊢" 30)
where
SkipT[intro!]: "(0, (0, ∞)) ⊢ SKIP" |
IncT[intro!]: "(0, (0, ∞)) ⊢ x++" |
DecT[intro!]: "(0, (0, ∞)) ⊢ x--" |
SleepT[intro!]: "(0, (0, 0)) ⊢ SLEEP" |
UnlockT[intro!]:"(-1, (1, ∞)) ⊢ UNLOCK x" |
LockT[intro!]: "(1, (0, ∞)) ⊢ LOCK x" |
SeqT[intro!]: "⟦(i⇩1, (r⇩1, u⇩1)) ⊢ c⇩1; (i⇩2, (r⇩2, u⇩2)) ⊢ c⇩2;
Fin (max (int r⇩2) (int r⇩1 + i⇩1))
≤ min (to_eint u⇩2) (to_eint u⇩1 + Fin i⇩1);
r = nat (max (int r⇩2 - i⇩1) (int r⇩1));
u = to_enat (min (to_eint u⇩2 - Fin i⇩1) (to_eint u⇩1));
i = i⇩1 + i⇩2⟧
⟹ (i, (r, u)) ⊢ c⇩1;; c⇩2" |
CallT[intro!]: "Γ ⊢ funcs f ⟹ Γ ⊢ CALL f" |
WhileT[intro!]: "⟦(0, (r, u)) ⊢ c⟧ ⟹ (0, (r, u)) ⊢ (WHILE x ≠ 0 DO c)"
```
I was able to prove that
```
(0, (0, 0)) ⊢ SLEEP;; LOCK ''a'';; UNLOCK ''b''
```
but also able to show that
```
¬ ⊨ SLEEP;; LOCK ''a'';; UNLOCK ''b''
```
Which is a counterexample to the correctness theorem that I tried to prove:
```
(i, (s, e)) ⊢ c ⟹ ⊨ c
```
My questions:
1. is the definition of `sound` what you also have in mind?
2. if I should not change `sound`, what should I change?
If I am thinking correctly, this should not be a real issue, since in Rust every lock that is unlocked needs to be locked first, which means that the count will be `> 0` when the function is called, which klint will deny.
Gary: We can do
```
| Sleep: "can_sleep s ⟹ (SLEEP, s) → (SKIP, s)"
| SleepV: "¬ can_sleep s ⟹ (SLEEP, s) → (ABORT, s)"
| SeqAbort: "(ABORT;;c, s) → (ABORT, s)"
definition good :: "'a com ⇒ bool"
where "⊨ c ≡ ∃l. ∀v. ¬(∃s. (c, (l, v)) →* (ABORT, s))"
```
so UB will stuck and atomic context violation will abort.
Alice suggested something that Gary thinks is similar to the one above, but swap the ABORT and stuck states?
## Miscellaneous
<!-- stuff that does not fit into other categories -->
Sign in with Wallet
Connect another wallet