Name
Abstract | ||
|---|---|---|
We develop a rigorous semantics for Power and ARM multiprocessor programs, including their relaxed memory model and the behaviour of reasonable fragments of their instruction sets. The semantics is mechanised in the HOL proof assistant. This should provide a good basis for informal reasoning and formal verification of low-level code for these weakly consistent architectures, and, together with our x86 semantics, for the design and compilation of high-level concurrent languages. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1145/1481839.1481842 | DAMP |
Keywords | Field | DocType |
high-level concurrent language,arm multiprocessor machine code,hol proof assistant,arm multiprocessor program,x86 semantics,informal reasoning,instruction set,rigorous semantics,low-level code,good basis,formal verification,powerpc,reliability,semantics,theory,standardization,arm,memory model,proof assistant | HOL,Operational semantics,Programming language,Computer science,Instruction set,Denotational semantics,Theoretical computer science,Machine code,Semantics,Formal verification,Proof assistant | Conference |
Citations | PageRank | References |
43 | 1.58 | 15 |
Authors | ||
7 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jade Alglave | 1 | 608 | 26.53 |
| Anthony Fox | 2 | 46 | 2.32 |
| Samin Ishtiaq | 3 | 147 | 15.28 |
| Magnus O. Myreen | 4 | 621 | 35.67 |
| Susmit Sarkar | 5 | 744 | 30.76 |
| Peter Sewell | 6 | 1446 | 68.16 |
| francesco zappa nardelli | 7 | 654 | 28.80 |