Meeting 2023-11-22

# Meeting 2023-11-22  ## Critical  ## Status Reports  ### 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  ### 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