The temporal semantics of concurrent programs Export

@article{citeulike:3204015, abstract = {The formalism of Temporal Logic is suggested as an appropriate tool for formalizing the semantics of concurrent programs. A simple model of concurrent program is presented in which n processors are executing concurrent n disjoint programs under a shared memory environment. The semantics of such a program specifies the class of state sequences which are admissible as proper execution sequences under the program. The two main criteria which are required are 1. (a) Each state is obtained from its predecessor in the sequence by exactly one processor performing an atomic instruction in its process. 2. (b) Fair Scheduling: no processor which is infinitely often enabled will be indefinitely delayed. The basic elements of Temporal Logic are introduced in a particular logic framework DX. The usefulness of Temporal Logic notation in describing properties of concurrent programs is demonstrated. A construction is then given for assigning to a program P a temporal formula W(P) which is true on all proper execution sequences of P. In order to prove that a program P possesses a property R1, one has only to prove the implications W(P)[superset or implies]R. An example of such proof is given. It is then demonstrated that specification of the Temporal character of the program's behavior is absolutely essential for the unambiguous understanding of the meaning of programming constructs.}, author = {Pnueli, Amir}, citeulike-article-id = {3204015}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/0304-3975(81)90110-9}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B6V1G-45W3WRM-2B/2/ff4d5447d3bfbe872a8aabbc48fc0417}, doi = {10.1016/0304-3975(81)90110-9}, journal = {Theoretical Computer Science}, keywords = {temporal-logic}, number = {1}, pages = {45--60}, posted-at = {2008-09-08 07:21:27}, priority = {2}, title = {The temporal semantics of concurrent programs}, url = {http://dx.doi.org/10.1016/0304-3975(81)90110-9}, volume = {13}, year = {1981} }

TY - JOUR ID - citeulike:3204015 L3 - citeulike-article-id:3204015 N2 - The formalism of Temporal Logic is suggested as an appropriate tool for formalizing the semantics of concurrent programs. A simple model of concurrent program is presented in which n processors are executing concurrent n disjoint programs under a shared memory environment. The semantics of such a program specifies the class of state sequences which are admissible as proper execution sequences under the program. The two main criteria which are required are 1. (a) Each state is obtained from its predecessor in the sequence by exactly one processor performing an atomic instruction in its process. 2. (b) Fair Scheduling: no processor which is infinitely often enabled will be indefinitely delayed. The basic elements of Temporal Logic are introduced in a particular logic framework DX. The usefulness of Temporal Logic notation in describing properties of concurrent programs is demonstrated. A construction is then given for assigning to a program P a temporal formula W(P) which is true on all proper execution sequences of P. In order to prove that a program P possesses a property R1, one has only to prove the implications W(P)[superset or implies]R. An example of such proof is given. It is then demonstrated that specification of the Temporal character of the program's behavior is absolutely essential for the unambiguous understanding of the meaning of programming constructs. IS - 1 JF - Theoretical Computer Science EP - 60 TI - The temporal semantics of concurrent programs VL - 13 SP - 45 KW - temporal-logic AU - Pnueli, Amir PY - 1981/// UR - http://dx.doi.org/10.1016/0304-3975(81)90110-9 ER -