کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4951439 | 1364355 | 2016 | 13 صفحه PDF | دانلود رایگان |
- A new concept is introduced for use in specifying and reasoning about concurrent programs.
- Use of the notation for “possible values” fits well with Rely/Guarantee methods.
- The use of the notation and inference rules is illustrated on Simpson's “four-slot” algorithm.
An important issue in concurrency is interference. This issue manifests itself in both shared-variable and communication-based concurrency - this paper focuses on the former case where interference is caused by the environment of a process changing the values of shared variables. Rely/guarantee approaches have been shown to be useful in specifying and reasoning compositionally about concurrent programs. This paper explores the use of a “possible values” notation for reasoning about variables whose values can be changed multiple times by interference. Apart from the value of this concept in providing clear specifications, it offers a principled way of avoiding the need for some auxiliary (or ghost) variables whose unwise use can destroy compositionality.
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 85, Issue 5, Part 2, August 2016, Pages 972-984