GitHub topics: weak-memory-models
binary-translation/lasagne-proofs
Architecture mapping proofs written in Agda for the paper "Lasagne: A Static Binary Translator for Weak Memory Model Architectures"
Language: Agda - Size: 163 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 13 - Forks: 2
goens/lost-pop-lean
POP Memory Model in Lean
Language: Lean - Size: 552 KB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 8 - Forks: 0
weakmemory/imm
Intermediate Memory Model (IMM) and compilation correctness proofs for it
Language: Coq - Size: 1.52 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 23 - Forks: 3
rymrg/rocker
Rocker: Robustness Checker
Language: D - Size: 142 KB - Last synced at: almost 2 years ago - Pushed at: almost 5 years ago - Stars: 11 - Forks: 1
dfava/mmgo
Operational Semantics of a Weak Memory Model with Channel Synchronization
Language: Python - Size: 82 KB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 2 - Forks: 1
PavlosMak/LLVM-Fence-Insertion
An automatic fence insertion pass for LLVM based on ILP constraints.
Language: LLVM - Size: 55.7 MB - Last synced at: over 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
