---
# System prepended metadata

title: Meeting 2023-11-22
tags: [meeting notes]

---

# Meeting 2023-11-22
<!-- 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 -->

### New Build system

Benno: What does the status on this look like?

Benno: @ojeda I would like to use it for `pin-init`, but if you think that you still need some more time, then I would do another update without it.

Miguel will send the patch for testing to Benno to do it in the current Kbuild system.

Current plan: probably something based on TOML, written in Rust, gets invoked by Kbuild. Miguel wants to integrate some attributes currently specified in source file into this build system.


### Memory modeling

https://github.com/rust-lang/unsafe-code-guidelines/issues/476

## Discussion Questions
<!-- Anything that requires lengthy discussion/more general questions also fit here -->

### Abstraction registry page

https://github.com/Rust-for-Linux/rust-for-linux.com/pull/12

Miguel: It would be ideal that the people working on the abstractions also update the table themselves. A disclaimer would be nice too.

### MMIO Typed Access

https://rust-for-linux.zulipchat.com/#narrow/stream/291565-Help/topic/Accessing.20memory.20mapped.20registers.20via.20struct

Tock: https://github.com/tock/tock
Tock registers: https://docs.rs/tock-registers/latest/tock_registers/

some discussion about code generator vs macros.

### 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.


Boqun: maybe adding a list in the type to track the current held locks

Lock
```
(i, (s, e), ls) ⊢ c
-----------------------------------
(i + 1, (s, e), l:ls) ⊢ c;; LOCK l
```
Unlock (only support reverse orderred unlock)
```
(i+1, (s, e), l:ls) ⊢ c
-------------------------------
(i, (s, e), ls) ⊢ c;; UNLOCK l
```

## Miscellaneous
<!-- stuff that does not fit into other categories -->
