检索结果-内蒙古大学图书馆

An observationally complete program logic for imperative higher-order functions

THEORETICAL COMPUTER SCIENCE 2014年 517卷 75-101页

作者： Honda, Kohei Yoshida, Nobuko Berger, Martin Univ London Dept Comp Sci London WC1E 7HU England Univ London Imperial Coll Sci Technol & Med Dept Comp London SW7 2AZ England Univ Sussex Dept Informat Brighton BN1 9RH E Sussex England

We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state. (C) 2013 Elsevier B.V. All rights reserved.

关键词： Completeness Characteristic formulae program logic Higher-order function Imperative programming Observational equivalence

来源：评论

学校读者我要写书评

暂无评论

A Compositional Theory of Linearizability

引用

JOURNAL OF THE ACM 2024年第2期71卷 1-107页

作者： Vale, Arthur Oliveira Shao, Zhong Chen, Yixuan Yale Univ New Haven CT USA Yale Univ Dept Comp Sci POB 208285 New Haven CT 06520 USA

Compositionality is at the core of programming languages research and has become an important goal toward scalable verification of large systems. Despite that, there is no compositional account of linearizability, the gold standard of correctness for concurrent objects. In this article, we develop a compositional semantics for linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, and this is themain discovery of ourwork, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory of linearizability, providing novel, simple, algebraic proofs of the locality property and of an analogue of the equivalence with observational refinement. We show our techniques can be used in practice by connecting our semantics with a simple program logic that is nonetheless sound concerning this generalized linearizability.

关键词： Linearizability game semantics concurrency program logic

来源：评论

学校读者我要写书评

暂无评论

Cerise: program Verification on a Capability Machine in the Presence of Untrusted Code

引用

JOURNAL OF THE ACM 2024年第1期71卷 1-59页

作者： Georges, Aina Linn Gueneau, Armael Van Strydonck, Thomas Timany, Amin Trieu, Alix Devriese, Dominique Birkedal, Lars Max Planck Inst Software Syst Campus E1 5 D-66123 Saarbrucken Germany Univ Paris Saclay CNRS Lab Methodes Formelles ENS Paris SaclayInria Bat 650 Ada LovelaceRue Raimond Castaing F-91190 Gif Sur Yvette France Katholieke Univ Leuven Imec Distrinet Celestijnenlaan 200A Bus 2402 B-3001 Heverlee Belgium Aarhus Univ Abogade 34 DK-8200 Aarhus N Denmark ANSSI 51 Blvd Tour Maubourg F-75700 Paris 07 SP France

A capability machine is a type of CPU allowing fine-grained privilege separation using capabilities, machine words that represent certain kinds of authority. We present a mathematical model and accompanying proof methods that can be used for formal verification of functional correctness of programs running on a capability machine, even when they invoke and are invoked by unknown (and possibly malicious) code. We use a program logic called Cerise for reasoning about known code, and an associated logical relation, for reasoning about unknown code. The logical relation formally captures the capability safety guarantees provided by the capability machine. The Cerise program logic, logical relation, and all the examples considered in the paper have been mechanized using the Iris program logic framework in the Coq proof assistant. The methodology we present underlies recent work of the authors on formal reasoning about capability machines [Georges et al. 2021;Skorstengaard et al. 2019a;Van Strydonck et al. 2022], but was left somewhat implicit in those publications. In this paper we present a pedagogical introduction to the methodology, in a simpler setting (no exotic capabilities), and starting from minimal examples. We work our way up to new results about a heap-based calling convention and implementations of sophisticated object-capability patterns of the kind previously studied for high-level languages with object-capabilities, demonstrating that the methodology scales to such reasoning.

关键词： Capability machines capability safety universal contracts program logic separation logic CHERI

来源：评论

学校读者我要写书评

暂无评论

On Extending Incorrectness logic with Backwards Reasoning

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2025年第POPL期9卷 391-415页

作者： Verbeek, Freek Sefat, Md Syadus Fu, Zhoulai Ravindran, Binoy Open Univ Netherlands Heerlen Netherlands Virginia Tech Blacksburg VA USA SUNY Stony Brook Stony Brook NY USA

This paper studies an extension of O'Hearn's incorrectness logic (IL) that allows backwards reasoning. IL in its current form does not generically permit backwards reasoning. We show that this can be mitigated by extending IL with underspecification. The resulting logic combines underspecification (the result, or postcondition, only needs to formulate constraints over relevant variables) with underapproximation (it allows to focus on fewer than all the paths). We prove soundness of the proof system, as well as completeness for a defined subset of presumptions. We discuss proof strategies that allow one to derive a presumption from a given result. Notably, we show that the existing concept of loop summaries - closed-form symbolic representations that summarize the effects of executing an entire loop at once - is highly useful. The logic, the proof system and all theorems have been formalized in the Isabelle/HOL theorem prover.

关键词： incorrectness logic backwards reasoning program logic

来源：评论

学校读者我要写书评

暂无评论

An Axiomatic Basis for Computer programming on the Relaxed Arm-A Architecture: The AxSL logic

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2024年第POPL期8卷 604-637页

作者： Hammond, Angus Liu, Zongyuan Perami, Thibaut Sewell, Peter Birkedal, Lars Pichon-Pharabod, Jean Univ Cambridge Comp Lab JJ Thomson Ave Cambridge CB3 0FD England Aarhus Univ Abogade 34 DK-8200 Aarhus Denmark

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.

关键词： relaxed memory models program logic separation logic Arm Iris

来源：评论

学校读者我要写书评

暂无评论

Advancing the decadal plan for the science of nutrition: Progressing a framework for implementation

引用

NUTRITION & DIETETICS 2024年第2期81卷 133-148页

作者： Truby, Helen Allman-Farinelli, Margaret Beck, Eleanor J. Beckett, Emma L. Bondonno, Catherine Dordevic, Aimee L. Livingstone, Katherine M. Willcox, Jane Wilkinson, Shelley A. Univ Queensland Brisbane Australia Univ Sydney Sydney Australia Univ New South Wales Sydney Australia FoodiQ Global Sydney Australia Edith Cowan Univ Joondalup Australia Monash Univ Melbourne Australia Deakin Univ Melbourne Australia Royal Womens Hosp Parkville Australia Mater Hlth Brisbane Australia Univ Sydney Fac Med & Hlth Charles Perkins Ctr Susan Wakil Sch Nursing & Midwifery Sydney NSW 2006 Australia

Aims: In 2019, the Australian Academy of Science in collaboration with the nutrition community published the decadal plan for the science of nutrition. This article aims to review progress towards each of its pillar goals (societal determinants, nutrition mechanisms, precision and personalised nutrition, and education and training) and two enabling platforms (a national data capability and a trusted voice for nutrition science), prioritise actions, and conceptualise program logic implementation models. This process also brought together public health nutrition researchers to reflect on societal determinants of health, and advise how the next 5 years of the decadal plan could reflect contemporary issues. Methods: Two engagement events, in 2023, brought together experienced and mid- and early-career nutrition professionals for co-creation of implementation logic models. Results: One hundred and nine early and mid-career professionals were involved. A revised model for the decadal plan pillars emerged from synthesis of all logic models. This new model integrated the precision and personalised nutrition pillar with nutrition mechanisms pillar. These combined pillars build towards the national data capability enabling platform and created new cross-cutting themes for education and training. The need arose for greater focus on respectful engagement with Aboriginal and Torres Strait Islander communities and sustained effort to build cross-disciplinary collaboration to realise the plan's societal determinants goals. A new alliance for nutrition science is proposed to become a unified advocacy voice and build trust in nutrition professionals. Conclusions: A programmatic approach provides a road map for implementing the decadal plan for the final 5 years.

关键词： decadal plan implementation nutrition science program logic

来源：评论

学校读者我要写书评

暂无评论

A Compositional Theory of Linearizability

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2023年第POPL期7卷 1089-1120页

作者： Vale, Arthur Oliveira Shao, Zhong Chen, Yixuan Yale Univ New Haven CT 06520 USA

Compositionality is at the core of programming languages research and has become an important goal toward scalable verification of large systems. Despite that, there is no compositional account of linearizability, the gold standard of correctness for concurrent objects. In this paper, we develop a compositional semantics for linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, and this is the main discovery of our work, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory of linearizability, providing novel, simple, algebraic proofs of the locality property and of an analogue of the equivalence with observational refinement. We show our techniques can be used in practice by connecting our semantics with a simple program logic that is nonetheless sound concerning this generalized linearizability.

关键词： linearizability game semantics concurrency program logic

来源：评论

学校读者我要写书评

暂无评论

Leveraging Rust Types for program Synthesis

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2023年第PLDI期7卷 1414-1437页

作者： Fiala, Jonas Itzhaky, Shachar Muller, Peter Polikarpova, Nadia Sergey, Ilya Swiss Fed Inst Technol Dept Comp Sci Zurich Switzerland Technion Haifa Israel Univ Calif San Diego San Diego CA USA Natl Univ Singapore Singapore Singapore

The Rust type system guarantees memory safety and data-race freedom. However, to satisfy Rust's type rules, many familiar implementation patterns must be adapted substantially. These necessary adaptations complicate programming and might hinder language adoption. In this paper, we demonstrate that, in contrast to manual programming, automatic synthesis is not complicated by Rust's type system, but rather benefits in two major ways. First, a Rust synthesizer can get away with significantly simpler specifications. While in more traditional imperative languages, synthesizers often require lengthy annotations in a complex logic to describe the shape of data structures, aliasing, and potential side effects, in Rust, all this information can be inferred from the types, letting the user focus on specifying functional properties using a slight extension of Rust expressions. Second, the Rust type system reduces the search space for synthesis, which improves performance. In this work, we present the first approach to automatically synthesizing correct-by-construction programs in safe Rust. The key ingredient of our synthesis procedure is Synthetic Ownership logic, a new program logic for deriving programs that are guaranteed to satisfy both a user-provided functional specification and, importantly, Rust's intricate type system. We implement this logic in a new tool called RusSOL. Our evaluation shows the effectiveness of RusSOL, both in terms of annotation burden and performance, in synthesizing provably correct solutions to common problems faced by new Rust developers.

关键词： program synthesis program logic Rust type systems

来源：评论

学校读者我要写书评

暂无评论

The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation logic 25

The Nextgen Modality: A Modality for Non-Frame-Preserving Up...

引用

14th Conference on Certified programs and Proofs

作者： Vindum, Simon Friis Georges, Aina Linn Birkedal, Lars Aarhus Univ Dept Comp Sci Aarhus Denmark Aarhus Univ Aarhus Denmark

ISBN: (纸本)9798400713477

As separation logic is a logic of resources, the way in which resources can soundly change and be updated is a fundamental aspect. Such changes have typically been restricted to certain local or frame-preserving updates. However, recently we have seen separation logics where the restriction to frame-preserving updates seems to be a hindrance towards achieving the ideal program reasoning rules. In this, paper we propose a novel nextgen modality that enables reasoning across generations where each generational change can update resources in ways that are non-local and non-frame-preserving. We implement the idea as an extension to the Iris base logic, which enriches Iris with an entirely new capability: the ability to make non-frame-preserving updates to ghost state. We show that two existing Iris modalities are special cases of the nextgen modality. Our "extension" can thus also be seen as a generalization and simplification of the Iris base logic. To demonstrate the utility of the nextgen modality we use it to construct a separation logic for a programming language with explicit stack allocation and with a return operation that clears entire stack frames. The nextgen modality is used to great effect in the reasoning rule for return, where a modular and practical reasoning rule is otherwise out of reach. This is the first separation logic for a high-level programming language with stack allocation. We sketch ideas for future work in other domains where we think the nextgen modality can be useful.

关键词： separation logic Iris Coq program logic modality

来源：评论

学校读者我要写书评

暂无评论

Spirea: A Mechanized Concurrent Separation logic for Weak Persistent Memory

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2023年第OOPSLA期7卷 632–657页

作者： Vindum, Simon Friis Birkedal, Lars Aarhus Univ Dept Comp Sci Aarhus Denmark

Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory. A wealth of algorithms and libraries has been developed to explore this exciting technology. As noted by others, this has led to a significant verification gap. Towards closing this gap, we present Spirea, the first concurrent separation logic for verification of programs under a weak persistent memory model. Spirea is based on the Iris and Perennial verification frameworks, and by combining features from these logics with novel techniques it supports high-level modular reasoning about crash-safe and thread-safe programs and libraries. Spirea is fully mechanized in the Coq proof assistant and allows for interactive development of proofs with the Iris Proof Mode. We use Spirea to verify several challenging examples with modular specifications. We show how our logic can verify thread-safety and crash-safety of non-blocking durable data structures with null-recovery, in particular the Treiber stack and the Michael-Scott queue adapted to persistent memory. This is the first time durable data structures have been verified with a program logic.

关键词： weak memory persistent memory non-volatile memory persistency program verification program logic Iris

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：