Modal assertions for actor correctness
Modal assertions for actor correctness
复制标题
参与者正确性的模态断言
DOI：
10.1145/3358499.3361221
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Gordon, Colin S.
中科院分区：
文献类型：
--
作者：
Gordon, Colin S.
参与者模型是一种成熟的方法，用于模块化设计和实现并发和/或分布式系统，并在行业中得到越来越多的采用。但是针对执行元程序的演绎验证仍未得到充分的探索；可以使用一般的并发逻辑，但该逻辑复杂且具有丰富的特征来推理执行元程序模型所要避免的行为。我们探索了一种相对轻量级的方法来扩展系统以证明连续程序的正确性(目前，假设没有错误)。我们借鉴了混合逻辑的思想，这是一种用于声明断言在模型中的特定点(在本例中是特定参与者的本地状态)为真的模式逻辑。为了使这样的断言有用，我们在本地参与者状态上使用依赖-保证风格的推理来稳定它们，并且只允许将这些断言的稳定版本发送给其他参与者。通过谨慎地限制某个参与者断言命题为真的形成，我们避免了参与者显式地处理彼此的依赖-保证关系的需要。最后，我们认为，该方法只需要适度的调整，而不是将传统的顺序技术应用于具有不可变消息的参与者，而是将大多数逻辑实现为Dafny库。
The actor model is a well-established way to approach to modularly designing and implementing concurrent and/or distributed systems, seeing increasing adoption in industry. But deductive verification tailored to actor programs remains underexplored; general concurrent logics could be used, but the logics are complex and full of features to reason about behaviors the actor model strives to avoid.We explore a relatively lightweight approach of extending a system for proving sequential program correctness with means to prove safety properties of actor programs (currently, assuming no faults). We borrow ideas from hybrid logic, a modal logic for stating assertions are true at a particular point in a model (in this case, a particular actor’s local state). To make such assertions useful, we stabilize them using rely-guarantee-style reasoning over local actor states, and only permit sending stable versions of these assertions to other actors. By carefully restricting the formation of assertions that a proposition is true at a certain actor, we avoid the need for actors to handle each others’ rely-guarantee relations explicitly. Finally, we argue that the approach requires only modest adjustments beyond applying traditional sequential techniques to actors with immutable messages, by implementing most of the logic as a Dafny library.
登录
查看更多内容
DOI：
--
发表时间：
2018
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Ankush Desai;Amar Phanishayee;S. Qadeer;S. Seshia
通讯作者：
S. Seshia
动态逻辑的自然演绎方法
DOI：
10.1007/3-540-61780-9_69
发表时间：
1995
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
F. Honsell;Marino Miculan
通讯作者：
Marino Miculan
基于集合约束的参与者分析
DOI：
10.1007/978-0-387-35261-9_8
发表时间：
1997
期刊：
Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control
影响因子：
--
作者：
Jean;M. Pantel;P. Sallé
通讯作者：
P. Sallé
影响因子：
1.3
作者：
Gordon, Colin S.;Ernst, Michael A.;Parkinson, Matthew J.
通讯作者：
Parkinson, Matthew J.
具有跟踪语义的动态逻辑
DOI：
10.1007/978-3-642-38574-2_22
发表时间：
2013
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
Bernhard Beckert;Daniel Grahl
通讯作者：
Daniel Grahl