Extending the theory of Owicki and Gries with a logic of progress
This paper describes a logic of progress for concurrent programs. The logic is based on that of UNITY, molded to fit a sequential programming model. Integration of the two is achieved by using auxiliary variables in a systematic way that incorporates program counters into the program text. The rules...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2006-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/2260/pdf |
| _version_ | 1797268742592266240 |
|---|---|
| author | Brijesh Dongol Doug Goldson |
| author_facet | Brijesh Dongol Doug Goldson |
| author_sort | Brijesh Dongol |
| collection | DOAJ |
| description | This paper describes a logic of progress for concurrent programs. The logic
is based on that of UNITY, molded to fit a sequential programming model.
Integration of the two is achieved by using auxiliary variables in a systematic
way that incorporates program counters into the program text. The rules for
progress in UNITY are then modified to suit this new system. This modification
is however subtle enough to allow the theory of Owicki and Gries to be used
without change. |
| first_indexed | 2024-04-25T01:37:19Z |
| format | Article |
| id | doaj.art-0e8be823b6114c249ddd9c13c8fab24e |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:19Z |
| publishDate | 2006-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-0e8be823b6114c249ddd9c13c8fab24e2024-03-08T08:34:30ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742006-03-01Volume 2, Issue 110.2168/LMCS-2(1:6)20062260Extending the theory of Owicki and Gries with a logic of progressBrijesh Dongolhttps://orcid.org/0000-0003-0446-3507Doug GoldsonThis paper describes a logic of progress for concurrent programs. The logic is based on that of UNITY, molded to fit a sequential programming model. Integration of the two is achieved by using auxiliary variables in a systematic way that incorporates program counters into the program text. The rules for progress in UNITY are then modified to suit this new system. This modification is however subtle enough to allow the theory of Owicki and Gries to be used without change.https://lmcs.episciences.org/2260/pdfcomputer science - logic in computer scienced.2.4d.3.1f.3.1 |
| spellingShingle | Brijesh Dongol Doug Goldson Extending the theory of Owicki and Gries with a logic of progress Logical Methods in Computer Science computer science - logic in computer science d.2.4 d.3.1 f.3.1 |
| title | Extending the theory of Owicki and Gries with a logic of progress |
| title_full | Extending the theory of Owicki and Gries with a logic of progress |
| title_fullStr | Extending the theory of Owicki and Gries with a logic of progress |
| title_full_unstemmed | Extending the theory of Owicki and Gries with a logic of progress |
| title_short | Extending the theory of Owicki and Gries with a logic of progress |
| title_sort | extending the theory of owicki and gries with a logic of progress |
| topic | computer science - logic in computer science d.2.4 d.3.1 f.3.1 |
| url | https://lmcs.episciences.org/2260/pdf |
| work_keys_str_mv | AT brijeshdongol extendingthetheoryofowickiandgrieswithalogicofprogress AT douggoldson extendingthetheoryofowickiandgrieswithalogicofprogress |