An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic

data/desc.txt

@@ -1,3 +1,3 @@
-Embedding by Unembedding
-Matsuda, Kazutaka, et al. “Embedding by Unembedding.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 1–47. Crossref, https://doi.org/10.1145/3607830.
-Embedding is a language development technique that implements the object language as a library in a host language. There are many advantages of the approach, including being lightweight and the ability to inherit features of the host language. A notable example is the technique of HOAS, which makes crucial use of higher-order functions to represent abstract syntax trees with binders. Despite its popularity, HOAS has its limitations. We observe that HOAS struggles with semantic domains that cannot be naturally expressed as functions, particularly when open expressions are involved. Prominent examples of this include incremental computation and reversible/bidirectional languages. In this paper, we pin-point the challenge faced by HOAS as a mismatch between the semantic domain of host and object language functions, and propose a solution. The solution is based on the technique of unembedding , which converts from the finally-tagless representation to de Bruijn-indexed terms with strong correctness guarantees. We show that this approach is able to extend the applicability of HOAS while preserving its elegance. We provide a generic strategy for Embedding by Unembedding, and then demonstrate its effectiveness with two substantial case studies in the domains of incremental computation and bidirectional transformations. The resulting embedded implementations are comparable in features to the state-of-the-art language implementations in the respective areas.
+An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
+Hammond, Angus, et al. “An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.” Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, Jan. 2024, pp. 604–37. Crossref, https://doi.org/10.1145/3632863.
+Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the 'current' state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next. We present AxSL, a separation logic for the relaxed memory model of Arm-A, that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. Our approach is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other similar models, and for the combination of production concurrency models and full-scale ISAs.

data/history.txt

@@ -38,4 +38,5 @@ https://doi.org/10.1145/3622820
 https://doi.org/10.1145/3632907
 https://doi.org/10.1017/S0956796824000017
 https://doi.org/10.1145/3689739
-https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3632863

data/next.txt

@@ -1 +1 @@
-https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3632863

data/past.txt

@@ -1,4 +1,5 @@
 
 https://doi.org/10.1017/S0956796824000017
 https://doi.org/10.1145/3689739
-https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3632863

docs/index.md

@@ -25,7 +25,7 @@ The PL Reading Group is a regular meeting of [ΔΛΔ](https://augusta.presence.i
 | 1.  | January 17  | Knuth–Morris–Pratt illustrated  | UH 227 |
 | 2.  | January 24  | Fully Verified Instruction Scheduling  | TBD |
 | 3.  | January 31  | Embedding by Unembedding  | UH 227 |
-| 4.  | February 7  | Paper 4 discussion  | UH 227 |
+| 4.  | February 7  | An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic  | UH 227 |
 | 5.  | February 14 | Paper 5 discussion  | UH 227 |
 | 6.  | February 21 | Paper 6 discussion  | UH 227 |
 | 7.  | February 28 | Paper 7 discussion  | UH 227 |

docs/papers.md

@@ -1,3 +1,4 @@
 1. MOY, CAMERON. “Knuth–Morris–Pratt Illustrated.” Journal of Functional Programming, vol. 34, 2024. Crossref, <a href='https://doi.org/10.1017/S0956796824000017' target='_blank'>https://doi.org/10.1017/S0956796824000017</a>.
 2. Yang, Ziteng, et al. “Fully Verified Instruction Scheduling.” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA2, Oct. 2024, pp. 791–816. Crossref, <a href='https://doi.org/10.1145/3689739' target='_blank'>https://doi.org/10.1145/3689739</a>.
-3. Matsuda, Kazutaka, et al. “Embedding by Unembedding.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 1–47. Crossref, <a href='https://doi.org/10.1145/3607830' target='_blank'>https://doi.org/10.1145/3607830</a>.
+3. Matsuda, Kazutaka, et al. “Embedding by Unembedding.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 1–47. Crossref, <a href='https://doi.org/10.1145/3607830' target='_blank'>https://doi.org/10.1145/3607830</a>.
+4. Hammond, Angus, et al. “An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.” Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, Jan. 2024, pp. 604–37. Crossref, <a href='https://doi.org/10.1145/3632863' target='_blank'>https://doi.org/10.1145/3632863</a>.