From 34d2c054bbb2ebf0e93b0d4c33ee24c045024158 Mon Sep 17 00:00:00 2001 From: nkrusch <2580981+nkrusch@users.noreply.github.com> Date: Wed, 29 Jan 2025 14:13:41 +0000 Subject: [PATCH] [create-pull-request] automated change --- data/desc.txt | 6 +++--- data/history.txt | 3 ++- data/next.txt | 2 +- data/past.txt | 3 ++- docs/index.md | 2 +- docs/papers.md | 3 ++- 6 files changed, 11 insertions(+), 8 deletions(-) diff --git a/data/desc.txt b/data/desc.txt index ecfd8da..9b8b23f 100644 --- a/data/desc.txt +++ b/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. \ No newline at end of file +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. \ No newline at end of file diff --git a/data/history.txt b/data/history.txt index c2fe081..0c69aba 100644 --- a/data/history.txt +++ b/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 \ No newline at end of file +https://doi.org/10.1145/3607830 +https://doi.org/10.1145/3632863 \ No newline at end of file diff --git a/data/next.txt b/data/next.txt index a20d580..0a18861 100644 --- a/data/next.txt +++ b/data/next.txt @@ -1 +1 @@ -https://doi.org/10.1145/3607830 \ No newline at end of file +https://doi.org/10.1145/3632863 \ No newline at end of file diff --git a/data/past.txt b/data/past.txt index 779a28c..b17dbe6 100644 --- a/data/past.txt +++ b/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 \ No newline at end of file +https://doi.org/10.1145/3607830 +https://doi.org/10.1145/3632863 \ No newline at end of file diff --git a/docs/index.md b/docs/index.md index 5ef7203..afb36f0 100644 --- a/docs/index.md +++ b/docs/index.md @@ -30,7 +30,7 @@ Current [reading group policies](policies). | 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 | diff --git a/docs/papers.md b/docs/papers.md index 9550167..556be24 100644 --- a/docs/papers.md +++ b/docs/papers.md @@ -1,3 +1,4 @@ 1. MOY, CAMERON. “Knuth–Morris–Pratt Illustrated.” Journal of Functional Programming, vol. 34, 2024. Crossref, https://doi.org/10.1017/S0956796824000017. 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, https://doi.org/10.1145/3689739. -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, https://doi.org/10.1145/3607830. \ No newline at end of file +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, https://doi.org/10.1145/3607830. +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, https://doi.org/10.1145/3632863. \ No newline at end of file