C4: verified transactional objects
C4: verified transactional objects
复制标题
C4：经过验证的交易对象
DOI：
10.1145/3527324
复制
发表时间：
2022
影响因子：
--
通讯作者：
Zdancewic, Steve
中科院分区：
文献类型：
--
作者：
Lesani, Mohsen;Xia, Li-yao;Kaseorg, Anders;Bell, Christian J.;Chlipala, Adam;Pierce, Benjamin C.;Zdancewic, Steve
事务对象联合收割机结合了经典并发对象的性能和事务内存的高级可编程性。然而，验证事务对象的正确性是棘手的，需要同时推理经典的并发对象，这保证了单个方法的原子性-称为线性化的属性-以及软件事务内存库，这保证了用户定义的方法调用序列的原子性-或串行化。从熟悉的线性化概念和它的组合属性建立起来，允许证明两种库，沿着来自两种风格的定理的组合，以证明应用程序或进一步库的正确性。我们应用框架中的一个重要的案例研究，验证了一个事务集对象建立的经典和事务组件的技术oftransactional预测;证明是模块化的，分别推理的事务和非事务部分的实现。我们的方法的核心是在交互树上使用语法转换器，即，事务库，用于转换客户端代码以强制执行特定的同步规程。我们的框架和案例研究是机械化的Coq。
Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability.We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique oftransactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers oninteraction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.
登录
查看更多内容
DOI：
10.1007/978-3-319-08867-9_37
发表时间：
2014
期刊：
--
影响因子：
--
作者：
M. Lesani;T. Millstein;J. Palsberg
通讯作者：
J. Palsberg
在语义课程中通过混合嵌入跳过活页夹官僚机构（功能性珍珠）
影响因子：
--
作者：
A. Chlipala
通讯作者：
A. Chlipala
Java并发编程——设计原则和模式
DOI：
--
发表时间：
1997
期刊：
--
影响因子：
--
作者：
Doug Lea
通讯作者：
Doug Lea
Starling：带视图的轻量级并发验证
DOI：
10.1007/978-3-319-63387-9_27
发表时间：
2017
期刊：
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
影响因子：
--
作者：
Matt Windsor;Mike Dodds;Ben Simner;Matthew J. Parkinson
通讯作者：
Matthew J. Parkinson
DOI：
10.1145/2555243.2555283
发表时间：
2014-02
期刊：
Proceedings of the 19th ACM SIGPLAN symposium on Principles and practice of parallel programming
影响因子：
--
作者：
Ahmed Hassan;R. Palmieri;B. Ravindran
通讯作者：
Ahmed Hassan;R. Palmieri;B. Ravindran