Projects formalizing cache coherence and memory models?

Stream: lean4

[Zhuanhao Wu]

Hi, I'm wondering if anyone is aware of lean/lean4 projects that formalize the semantics of hardware cache coherence or memory models? I'm trying to come up with a formalization of these topics, and it would be great to have a reference of some kind. Any pointers would be appreciated!

[James Gallicchio]

I think you might struggle to find such projects in Lean; there are currently relatively few people formalizing CS theory/PL/FM in Lean.

However, I know that there are Coq formalizations of memory and cache models, and Coq formalizations can still be a good references for Lean formalization, since the type theory is mostly the same!

[Marcus Rossel]

@Andrés Goens ping

[Andrés Goens]

Yeah, @James Gallicchio is right that you'll find more projects in Coq (and that's a good reference).

I did formalize a few memory consistency models (operetional semantics) in this repo, it's not updated to the latest versions of Lean but that shouldn't be a big issue (will do that soon), but one big issue is that it's currently all formalized using bool and not prop for the preconditions, I can discuss that more if you're interested. I don't know that there's much in the way of declarative semantics (sometimes called "axiomatic"), but I'm looking into that too in the near future.

@Z. Wu are you looking to formalize something concrete? If you tell us more about it we might be able to give more concrete pointers

[Zhuanhao Wu]

@Andrés Goens Thanks, I think the link you sent seems a good start!
And yeah, i'm curious - are you using bool instead of prop for specific reasons?

Yes, and any pointers would be appreciated!

I'm mainly interested in formalizing coherence protocols and attach timestamp to them to reason about the worst-case latency of requests. And the formalization needs to capture hardware details such as arbitration between cores/transient states in the protocol.

And the long term goal is to study the interaction between the consistency model and the coherence/underlying hardware with respect to latency by connecting the coherence formalization and the consistency model.

[Andrés Goens]

Hey @Z. Wu , sorry, was on a bit of a holiday break not looking at Zulip too much :sweat_smile: I think the primary reason I went for bool was that it was simpler, I was doing some weird stuff with typeclasses to emulate a module system and honestly didn't understand Decidable that well when I started with that

That sounds like a really interesting project! In that case you porbably do want to reason about it operationally, right? So that you can reason about things like abstraction or bisimulation relations, etc. I think we don't have too many tools for working with operational semantics in Lean 4 yet (compared to e.g. Isabelle, where they can automatically derive the computability of a relation in many cases, etc), but it would probably be nice to build more of that infrastructure

[Zhuanhao Wu]

@Andrés Goens yeah, I can somehow relate to the bool vs prop issue in terms of ease of use!

Thank you for the pointers! I think I will definitely try to look at the bisimulation/abstraction. And I will probably also look at labeled transition systems and trace refinement.
And yeah, true, I wish we could have tools/library that automate things - I was reading the "concrete semantics" book and figured that there's plenty of things we could improve in lean4