To push our verification to the extreme, we should consider all the levels of concurrency (concurrent algorithms, weak memory models, multiprocessors). Not all of these are guaranteed to be doable in Verus, but we should at least learn and understand the extent to which the PL community has accomplished in concurrent reasoning.
This issue tracks a list of papers about concurrency verification, which I think is worth reading.
There are some other papers which I have not investigated yet or not so closely related: RusBelt, RustHornBelt, Stacked Borrows, Tree Borrows, etc. CertiKOS seems to take a different approach (concurrent certified abstraction layer, which seems closer to CompCert) that deviates from the Iris technology roadmap.
To push our verification to the extreme, we should consider all the levels of concurrency (concurrent algorithms, weak memory models, multiprocessors). Not all of these are guaranteed to be doable in Verus, but we should at least learn and understand the extent to which the PL community has accomplished in concurrent reasoning.
This issue tracks a list of papers about concurrency verification, which I think is worth reading.
VerusSync.tokenized_state_machineinVerusSync.There are some other papers which I have not investigated yet or not so closely related: RusBelt, RustHornBelt, Stacked Borrows, Tree Borrows, etc. CertiKOS seems to take a different approach (concurrent certified abstraction layer, which seems closer to CompCert) that deviates from the Iris technology roadmap.