Formal Reasoning about Actor Programs Using Temporal Logic

发布时间:2021-11-29 06:27:35

Formal Reasoning about Actor Programs Using Temporal Logic
OSL, Department of Computer Science University of Illinois at Urbana-Champaign 1304 W. Spring eld Avenue, Urbana, IL 61801, USA email: schacht@cs.uiuc.edu

Susanne Schacht

We here present an approach to reasoning about actor programs on the basis of temporal logic. Temporal logic is particularly appropriate for the speci cation of concurrent programs, but most known temporal logic proof systems for concurrent computations rely on imperative language constructs, ignoring, e.g., the creation of processes and the dynamic con guration of communication channels, which are crucial for actor based programming.

Abstract

This work was supported by a grant from DFG under account Ha2097/1-3.

1

1 Temporal logic as a tool for speci cation and veri cation
Temporal logic is particularly appropriate for reasoning about programs for which a corresponding statement in terms of their operational or denotational semantics is too ne-grained to make useful assertions about the overall behavior of a complex system. Using a temporal logic framework, safety properties (invariants like partial correctness, absence of deadlock, mutual exclusion etc.) and liveness properties (termination, total correctness, cycles) of concurrent programs can be shown without having to take implementational details into account 11, 2]. However, most temporal logic proof systems for concurrent computations rely on imperative language constructs. They take only a simple action language as a basis to build the program's states and ignore the creation of processes and the dynamic con guration of communication channels, issues that are crucial for object-oriented programming, in particular, the actor model of computation 4, 1]. We here present an approach to reasoning about actor programs on the basis of temporal logic. In Section 2, we will sketch the actor model and introduce a simple syntax for actor programs. In Section 3, we introduce a general temporal logic system and then adjust it to the describtion of actor computations in Section 4.

2 The actor model
An actor system consists of several concurrently processing objects, called actors, with the ability to asynchronously send messages to each other (messages are assumed to be bu ered in their receivers' mail queue). An actor program (for a simple syntax, cf. Fig. 11) consists of a set of actor de nitions as well as some initially created actors and messages sent to them.
::= f actorDef g action ::= defActor actorType (acquaintance ) methodDef endDef methodDef ::= meth messageKey(param )(action) action ::= action; action j send actor messageKey (actor ) j if cond then (action) else (action)] j let var be actor in (action) j become actor actor ::= self j nil j value j acquaintance j param j var j(create actorType(actor )) program actorDef

Figure 1: Syntax of a basic actor language Each actor de nition enumerates identi ers of other actors which an actor instantiated from that de nition will know about (the actor's acquaintances), and it de nes the actor's reaction to incoming messages (its behavior) by way of method de nitions. Each instantiated actor has a unique mail address (its identity). Upon receiving a message an actor performs a composite action the elementary actions of which are: sending further messages to other actors it knows about (send), creating new actors from actor de nitions, thus supplying their initial acquaintances (create), and specifying a new behavior and/or new acquaintances for itself (become). The replacement behavior de ned by a become action is e ective for the next message the actor accepts. Only a single become action can
1 Keywords are written in italics; actorType, messageKey, param, acquaintance and var denote identi ers; cond refers to a boolean expression; nil is the unde ned value, and value stands for a basic value (boolean, integer etc.)

2

let

be performed during the processing of a message. Additionally, we allow for local variables, using a expression for binding actors to identi ers (var) that can occur in the action following in. Several specialized kinds of formal semantics have been proposed for the actor model, usually based on the notion of events (processing of a single message at an actor) and tasks (pending events). Agha's operational semantics 1] assigns a tree of con gurations related by transitions to each program as its meaning. A con guration consists of a local states function and a set of unprocessed tasks, where the local states function maps actor addresses to behaviors. Tasks are functions as well, mapping a unique tag (an identi er created in order to distinguish between similar tasks) to pairs consisting of a target actor address and a message. Transitions between con gurations are determined by choosing one of several unprocessed tasks for execution: the e ects of processing of this task's message at its target are evaluated, giving a set of new tasks, a set of newly created actors and the replacement behavior for the target actor. This type of semantics depends on the existence of one (of several possible) global view(s) of the system: the con gurations describe all actors involved. From local orderings of message arrivals and a partial causal ordering among events (possible) global orderings are derived. Concurrency is modeled by interleaving 'atomic' events.

3 A basic temporal logic proof system
For the general part of our proof system, we will rst introduce a set of temporal logic future operators. They can be expressed in terms of each other, and we have chosen atnext as the basic operator. Informally, A atnext B means that A will hold at the next state at which B holds. Some derived operators that are used below are formally de ned in Fig. 2. `next', A; 'A will hold at the next state' `eventually', 3A; 'A holds now or it will hold at least at one of the following states' `always', 2A; 'A holds now and at all following states' `until', A U B; 'A will hold up to the rst state at which B holds which will eventually occur' The semantics of a (linear) propositional temporal logic language is given by a structure K which A 3A 2A AU B

$ $ $ $

A atnext true A _ :(false atnext A) :3:A B atnext (A ! B) ^ 3B

Figure 2: De nitions of future operators is a sequence of states and the valuation of atomic propositions at each state. The structure for a rst-order temporal logic consists of a structure for the rst-order kernel (all formulae containing no temporal operators) and a sequence of variable valuations. Ki (F) is the valuation of a formula F (at state i) as in classical FOL and, additionally, for the temporal operators: Ki(A atnext B) = t i Kj (B) = f for all j > i or Kk (A) = t for smallest k > i with Kk (B) = t Ki ( A) = t i Ki+1(A) = t Ki(3 A) = t i Kj (A) = t for some j i 3

We will use the axioms (plus all propositional tautologies) and the inference rules (modus ponens, next and induction) in Fig. 3 to build a proof system for temporal logic.

Ki(2 A) = t i Kj (A) = t for every j i Ki(A U B) = t i Kj (B) = t for some j i and Kk (A) = t for every k; i k < j
: A (A ! B) 2A 2:B A atnext B 8x A A $ :A ! ( A ! B) ! (A ^ 2A) ! A atnext B $ (B ! A) ^ (:B ! A atnext B) ! 8xA ! A if A contains no local variable, i.e., that can change over time.
modus ponens: A A induction: A !AB; A2! A ! B

next: A; AB! B

Figure 3: Axioms and Inference rules for the temporal logic The soundness of the deduction system, stating that any derivable formula is valid, viz. if ` A then j= A , can be proved by induction over the derivation of A, considering the cases of A being an axiom or A being derived using the inference rules. We do not prove the completeness of the system described so far, since in the next step we will restrict the derivable formulae anyway.

4 Axiomatization of the actor model
In order to adjust this system to the actor model and to construct the domain part of the proof system, the actor language we supply must provide the elements for building local, non-temporal propositions about con gurations which consist of pending tasks and a local states function. These will serve as fundamental state descriptions. Sequences of states will then be de ned by determining the consequences of one of the pending tasks. We assume a standard rst-order logic by which propositions about the bindings between identiers and values (i.e., actor addresses and basic values) and between actors and their de nitions can be expressed. Accordingly, we use predicates of arity one to indicate whether an identi er denotes an instance of a certain actor de nition and consider variable and acquaintance names as function symbols to indicate an actor's acquaintances. For tasks, we use the notation (a; m), with a denoting an actor address and m denoting a unique message (which consists of a key and various parameters; in addition, it can be annotated with an identi er i, if necessary). This way, a state proposition in the underlying logic consists of a complex proposition (i.e., a conjunction of basic propositions) about bindings of identi ers to values (addresses or basic values) and actors to de nitions, props, and a set of unprocessed tasks, tasks. For a program, the initial con guration consists of the binding proposition for the initially created actors and the set of initially created tasks. The e ects of processing a task turn up as the creation of new tasks and changes a ecting the binding properties. These include the adding of new propositions for newly created actors and changes to the propositions for acquaintances of the a ected actor as well as changes to its binding to a de nition via a become action (replacing the old propositions by the new ones). 4

A formal de nition for the state transition will be given below. Meanwhile, we express the e ects of processing a task (a; m) on props and tasks as e ects(a; m)(props, tasks), or even shorter as e ects(a; m). e ects(a; m)(props) denotes the local state proposition props after (a; m) has been processed, e ects(a; m)(tasks) denotes the new set tasks. The following axiom states that exactly one element (a; m) of tasks is processed at each step and no other changes on props and tasks are made than those caused by (a; m):
props ^ tasks = oldTasks 6= ; $ 9(a; m) 2 tasks 8(b; n) 2 tasks : (e ects (a; m)(props ) ^ tasks = e ects (a; m)(oldTasks ) ^ ((b; n) = (a; m) _ (b; n) 2 tasks ))

Fairness can then be included as an axiom of the proof system: any pending task will stay pending until eventually it is chosen for execution. Then, in the next state it will be removed from tasks and its e ects can be observed. Since no pending task can be canceled, this axiom is su cient to guarantee fair computations: (a; m) 2 tasks $ (a; m) 2 tasks ^ ((a; m) 2 tasks U (e ects (a; m) ^ (a; m) 2 tasks )) = From this, we can conclude that (a; m) 2 tasks ! 3((a; m) 2 tasks ^ e ects (a; m)) since

Ki(A ^ (A U B)) = t i

, ) ) ,

Ki(A) = t and Ki+1(A U B) Kj (B) = t for some j > i and Kk (A) = t for every k; i < k < j Km( B) = t and Km (A) = t with m = j ? 1 Km(A ^ B); m i Ki(3(A ^ B))

In order to reason about a particular program the e ects of each possible task must be taken into account using the initially created actors and sent messages as well as the de nitions which constitute the program. The local state of an actor a is determined by its binding to an actor de nition (roughly, we may say, its 'type') and the value of its acquaintances, both determined by the local propositions props. From a's de nition we take the method de nition for m's message key. The bindings of m's parameters can be found in props as well, as they must have been either acquaintances or variables of m's sender or newly created actors known from the previous steps of computation; these are denoted as parami;m . If no identi er of an actor is available (e.g., if it is created as a parameter for a message), we use a variable which can be regarded as being existentially quanti ed. With these conventions, e ects(a; m)(props, tasks) can be de ned in a straight forward way. The e ects of performing (a; m) on the set of pending tasks, tasks, are determined by identifying all send actions in the method's de nition that are actually performed (depending on a's state). The receivers and messages are combined to tasks and then added to tasks. Below, action(a; m) denotes the action that is the body of m's de nition at a.
e ects (a; m)(tasks ) := tasks n f(a; m)g newTasks (action (a; m)) with:

5

8 > f(b; n)g if action = send b n > > newTasks (act1 ) newTasks (act2 ) if action = act1 ; act2 > > newTasks (act1 ) if action = if cond then act1 else act2 < newTasks(action) := > and cond is true with regard to props > newTasks (act2 ) > > if action = if cond then act1 else act2 and cond is false > : ; else Furthermore, the e ects on the local propositions, props, concern newly created actors via create actions and changes on a via become. For any actor b created from a de nition D with initial acquaintances aqci bound to ai, D(b) and aqci (b) = ai are added to props. All elements of props concerning a itself are changed according to the occurrence of a become action. e ects (a; m)(props ) := props created (action (a; m)) new (action (a; m))nold (action (a; m)) with these de nitions of created, new, and old where action occurs in the de nition of m at a: 8 < fD(var); aqc1 (var) = a1 ; : : :; aqcn(var) = an g if action = let var = create D(a1 : : :an ) created(action) := : and analogous for any other occurrence of create
new(action) :=

fD(a); aqc1 (a) = a1 ; : : :; aqcn(a) = ang
if action = become

8 < fDprev (a); aqc1(a) = b1; : : :; aqck (a) = bk g if action = become create D(a1 : : :an) old(action) := : and Dprev (b1 : : :bk ) was the previous actor de nition of a For the initial con guration, tasks and props are determined from initially empty sets and the action occurring in the program following the actor de nitions (cf. Fig. 1, line 1).

create D(a1

: : :an )

5 Discussion
Our work clearly bene ts from previous work that has been done in the eld of applying temporal logics to concurrent program speci cation. Among the temporal approaches, the work of Manna and Pnueli 7] is fundamental; TLA 6] and UNITY 3] both are elaborated speci cation languages based on temporal logics. They all have in common that they concentrate on the temporal part of the speci cation and do not provide a deep treatment of single states. This is, however, crucial for actor programming, since an actor system, as a whole, cannot be described simply by sequences of atomic states or events. Adequate descriptions of actor systems must account for the complexity of objects and connections between objects, instead. Process calculi like CSP 5] or CCS 8] do not allow for changes of the underlying topologies of communication channels as they occur in object-oriented systems as an e ect of object creation. The -calculus 9], or other extensions of process calculi, e.g., the Object Calculus by Nierstrasz 10], overcome these limitations. They could then be used for the speci cation of actor systems, though they are not designed for it. But since they are very ne-grained, this can only be achieved in a rather complicated way. Our work is motivated by the search for a formal framework in which a large-scale application, namely a natural language parser whose implementation is based on the actor model, can be described and speci ed in a formally disciplined way. Temporal logics turns out to be very suitable to that purpose. We have shown how a general proof system for discrete linear temporal logic can be adjusted to describe the behavior of actor systems. 6

References
1] Agha, G. The structure and semantics of actor languages. In Foundations of Object-Oriented Languages. LNCS 489., de Bakker, de Roever, and Rozenberg, Eds. Berlin etc.: Springer, 1990, pp. 1{59. 2] Barringer, H. The use of temporal logic in the compositional speci cation of concurrent systems. In Temporal Logics and their Applications., A. Galton, Ed. London etc.: Academic Press, 1987, pp. 53{90. 3] Chandy, K., and Misra, J. Parallel Program Design. A Foundation. Addison-Wesley, Reading/MA, 1988. 4] Hewitt, C., and Baker, H. Actors and continuous functionals. In Proc. of the IFIP Working Conf. on Formal Description of Programming Concepts. (1978), E. Neuhold, Ed., Amsterdam etc.: North-Holland, pp. 367{390. 5] Hoare, C. Communicating Sequential Processes. Prentice-Hall, Englewood Cli s/NJ, 1985. 6] Lamport, L. The temporal logic of actions. Transactions on Programming Languages and Systems 16, 3 (May 1994), 872{923. 7] Manna, Z., and Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems. Springer, Berlin etc., 1992. 8] Milner, R. Communication and Concurrency. Prentice-Hall, Englewood Cli s/NJ, 1989. 9] Milner, R., Parrow, J., and Walker, D. A calculus of mobile processes, i/ii. Information and Computation 100, 1 (1992), 1{77. 10] Nierstrasz, O. Towards an object calculus. In ECOOP'91 - Proc. of the European Workshop on Object-Based Concurrent Computing. Geneva, Switzerland, July 15-16, 1991 (Berlin etc., 1992), M. Tokoro, O. Nierstrasz, P. Wegner, and A. Yonezawa, Eds., Springer. 11] Owicki, S., and Lamport, L. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems 4, 3 (1982), 455{495.

7


相关文档

  • Temporal reasoning about actor programs
  • Model checking linear temporal logic using tabled logic programming
  • Reasoning about Temporal Context using Ontology and Abductive Constraint Logic Programming
  • Proving properties of actor programs using temporal logic
  • Temporal logic and reasoning about actions
  • A stuttering closed temporal logic for modular reasoning about concurrent programs
  • Using Temporal Logic for Spatial Reasoning Temporalized Propositional Neighborhood Logic E
  • IT IS DECLARATIVE ON REASONING ABOUT LOGIC PROGRAMS
  • Reasoning About Web Services in a Temporal Action Logic
  • Temporal Relevant Logic as the Logic Basis for Reasoning about Dynamics of Concurrent Syste
  • 猜你喜欢

  • 八年级语文下册课件18吆喝 (共19张PPT)
  • 英文版——大话西游剧本。
  • 刍议新闻传播的制约因素与传播策略
  • Android App:获取屏幕旋转角度
  • 天津财经大学国际经济01.第一讲 绪论
  • 打造阳光心态培训课件课件
  • 动感时尚MG动画图文介绍宣传动态ppt模板
  • 汽油发动机起动困难原因分析与探微
  • 新生命的诞生(知识点整理)
  • 英国留学签证面试官常问问题
  • 【精品模板】c038TGp_education_diagram_v2文化教育类PPT模板
  • 公文写作提速的方法
  • 治疗老年人风湿痛的药酒
  • 2019年牛津译林版九年级英语 上册Unit 3 Teenage problems单元测试卷(含答案)
  • 【公文范文】大学生村官年度考核情况报告
  • 微信零钱提现手续费
  • 四川省2016年下半年监理工程师执业资格:工程师的口头指示试题
  • 老人怎样保护心脏
  • 期中考试语文反思作文
  • 【IT专家】为什么我的ajax请求将空对象发送到服务器
  • 汽机实操题集
  • 江西省金溪县第一中学2018_2019学年高二历史12月月考试题(含解析)
  • 益气熄风汤对高血压大鼠AngⅡ和ALD的干预作用
  • 运行Hadoop自带的wordcount单词统计程序
  • 幼儿简笔画:可怕的小恐龙
  • 湖南省益阳市2016-2017学年高一下学期3月月考试题 数学 Word版含答案
  • 云南省2018年保育员三级考试试题试卷及答案
  • (技术合同)设计委托合同书
  • 2011届高考政治第一轮复习课件9
  • 三星s8home键隐藏设置
  • 北师大版 二年级数学上册 《5.6回家路上》 精品PPT课件 (2)
  • 职业培训工作计划通用4篇
  • 初中语文阅读教学提问策略研究
  • 广州市声皇音响设备有限公司(企业信用报告)- 天眼查
  • 江苏省扬州市高邮市车逻镇九年级数学上册第1章一元二
  • 最新-市人大机关扶贫工作计划 精品
  • 05第五章 内燃机混合气的形成与燃烧partI
  • 2017_2018学年高中地理第三章防灾与减灾第一节自然灾害的监测与防御课件新人教版选修5
  • 【精品】最新组织变革中的HR战略
  • [小初高学*]XX六年级数学下册总复*第六单元集体备课上课学*上课学*教案
  • 2020年大学学生会各部门工作计划【精品】
  • 2014年1-6月青海省及全国农用氮、磷、钾化学肥料总计(折纯)月度产量
  • 电脑版