Concurrency primitives - augment with proofs?

Stream: lean4

[Gary Haussmann]

I'm thinking about implementing some simple multithreaded code in Lean with mutexes (via ffi). I thought it might be interesting/useful to leverage the theorem prover if possible - for example, using proofs to avoid deadlocks and/or ensure data consistency.
Does anyone have experience or suggestions on where to look for this? I found some papers on Hoare Logic and Rely-Guarantee but I have no idea if that is the right place to start.

[Matthew Ballard]

I would also love to see any existing experience/directions/info/thoughts here.

[Mario Carneiro]

Connecting real concurrency primitives with a lean model will not be a particularly natural fit, because the observable behaviors you are interested in are not part of the type theory natively. Your best bet is to have a grammar of primitive operations which can be instantiated into both a concurrency model (that you can reason about) as well as actual calls to mutexes / etc (which you can run). It might help to get more concrete about this, though, and give an example of a program that you would like to prove correct or an argument you would like to verify

[Gary Haussmann]

As an example I wanted to try and avoid deadlock via proof. I guess I would have a specific set of mutexes, sequences of lock/unlock operations representing the operations performed by the various threads, and then check all the possible interleaving of operations?
Ideally the 'grammar of primitive operations' would be a Monad so that I could integrate it with whatever other Monad(s) I'm using. In a Haskell effect system I would then write two interpreters: one to generate actual running code and one to generate a model for analysis. I'm not sure what the equivalent would be here.

[Mario Carneiro]

Sure, that works. I'm saying that you should write a toy version of that to see what representational issues arise. (Also, re: "check all the possible interleaving of operations", that's not how it works, this would be tremendously inefficient and not worthwhile unless you are a model checker. Instead you would ensure a property which makes it impossible to deadlock in general, and prove that.)

[Henrik Böving]

On this topic I recently watched this talk over here https://www.youtube.com/watch?v=ES1bhxcRDy0 and while I have no doubt this could be formalized in Lean I would be curious as to whether one could actually incorporate this into the language itself?

[Henrik Böving]

I'm of course very well aware of the extension capabilities of Lean 4 im just entirely uncertain how you would incorporate something entirely different like this