Abstract
One might think that specifying and reasoning about concurrent programs would be easier with more expressive languages. This paper questions that view. Clearly too weak a notation can mean that useful properties either cannot be expressed or their expression is unnatural. But choosing too powerful a notation also has its drawbacks since reasoning receives little guidance. For example, few would suggest that programming languages themselves provide tractable specifications. Both rely/guarantee methods and separation logic(s) provide useful frameworks in which it is natural to reason about aspects of concurrency. Rather than pursue an approach of extending the notations of either approach, this paper starts with the issues that appear to be inescapable with concurrency and—only as a response thereto—examines ways in which these fundamental challenges can be met. Abstraction is always a ubiquitous tool and its influence on how the key issues are tackled is examined in each case.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial JR (1996) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge
Abrial JR (2010) The event-B book. Cambridge University Press, Cambridge
Ashcroft EA, Manna Z (1971) Formalization of properties of parallel programs. In: Meltzer B, Michie D (eds) Machine intelligence, vol 6. Edinburgh University Press, Edinburgh, pp 17–41
ANSI (1976) Programming language PL/I. Technical report X3.53-1976, American National Standard
Bornat R, Amjad H (2010) Inter-process buffers in separation logic with rely-guarantee. Form Asp Comput 22(6): 735–772
Bornat R, Amjad H (2013) Explanation of two non-blocking shared-variable communication algorithms. Form Asp Comput 25(6): 893–931
Burckhardt S, Gotsman A, Musuvathi M, Yang H (2012) Concurrent library correctness on the TSO memory model. In: ESOP
Boyland J (2003) Checking interference with fractional permissions. In: Cousot R (ed) Static analysis, vol 2694 of LNCS. Springer, New York, pp 55–72
Back RJ, Sere K (1991) Stepwise refinement of action systems. Struct Program 12: 17–30
Back R-JR, von Wright J (1998) Refinement calculus: a systematic introduction. Springer, New York
Collette P, Jones CB (2000) Enhancing the tractability of rely/guarantee specifications in the development of interfering operations. In: Plotkin G, Stirling C, Tofte M (eds) Proof, language and interaction, vol 10. MIT Press, USA, pp 277–307
Coleman JW, Jones CB. (2007) A structural proof of the soundness of rely/guarantee rules. J Log Comput 17(4): 807–841
Coleman JW (2008) Constructing a tractable reasoning framework upon a fine-grained structural operational semantics. PhD thesis, Newcastle University
Cousot P (2008) The verification grand challenge and abstract interpretation. In: Meyer B, Woodcock J (eds) Verified software: theories, tools, experiments, vol 4171. Lecture notes in computer science. Springer, Berlin/Heidelberg, pp 189–201. doi:10.1007/978-3-540-69149-5_21
Dahl OJ, Dijkstra EW, Hoare CAR (1972) Structured programming. Academic Press, Dublin
Dodds M, Feng X, Parkinson M, Vafeiadis V (2009) Deny-guarantee reasoning. In: Castagna G (ed) Programming languages and systems, vol 5502. Lecture notes in computer science. Springer, Berlin/Heidelberg, pp 363–377
Dijkstra EW (1968) Letters to the editor: go to statement considered harmful. Commun ACM 11(3): 147–148
Dingel J (2000) Systematic parallel programming. PhD thesis, Carnegie Mellon University, CMU-CS-99-172
Dingel J (2002) A refinement calculus for shared-variable parallel and distributed programming. Form Asp Comput 14(2): 123–197
de Roever WP (2001) Concurrency verification: introduction to compositional and noncompositional methods. Cambridge University Press, Cambridge
da Rocha Pinto P, Dinsdale-Young T, Dodds M, Gardner P, Wheelhouse M (2011) A simple abstraction for complex concurrent indexes. In: Proceedings of the 2011 ACM international conference on object oriented programming systems languages and applications, pp 845–864. ACM
Dinsdale-Young T, Birkedal L, Gardner P, Parkinson M, Yang H (2013) Views: compositional reasoning for concurrent programs. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 287–300. ACM
Dinsdale-Young T, Dodds M, Gardner P, Parkinson MJ, Vafeiadis V (2010) Concurrent abstract predicates. In: Proceedings of the 24th European conference on object-oriented programming. Springer, Berlin, pp 504–528
Feng X (2009) Local rely-guarantee reasoning. In: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL’09. ACM, New York, pp 315–327
Feng X, Ferreira R, Shao Z (2007) On the relationship between concurrent separation logic and assume-guarantee reasoning. In: ESOP: programming languages and systems. Springer, New York, pp 173–188
Floyd RW (1967) Assigning meaning to programs. Math Asp Comput Sci 19: 19–32
Gotsman A, Cook B, Parkinson M, Vafeiadis V (2009) Proving that non-blocking algorithms don’t block. In: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL’09. ACM, New York, pp 16–28
Gotsman A, Yang H (2011) Liveness-preserving atomicity abstraction. In: ICALP
Hoang TS, Abrial JR (2010) Event-B decomposition for parallel programs. In: Frappier M, Glaesser U, Sarfraz K, Laleau R, Reeves S (eds) ABZ, vol 5977 of LNCS. Springer, New York, pp 319–333
Hayes IJ, Burns A, Dongol B, Jones CB (2013) Comparing degrees of non-deterministic in expression evaluation. Comput J 56(6): 741–755
Hayes IJ, Jones CB, Colvin RJ (2014) Laws and semantics for rely-guarantee refinement. Technical report CS-TR-1425, Newcastle University
Hoare T, Möller B, Struth G, Wehrman I (2011) Concurrent Kleene algebra and its foundations. J Log Algebra Program 80(6): 266–296
Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580, 583
Hoare CAR (1972) Towards a theory of parallel programming. In: Operating system techniques. Academic Press, Dublin, pp 61–71
Herlihy M, Wing JM (1990) Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst 12(3): 463–492
Jones CB (1980) Software development: a rigorous approach. Prentice Hall International, Englewood Cliffs
Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis, Oxford University. Printed as: Programming Research Group, Technical Monograph 25.
Jones CB (1983) Specification and design of (parallel) programs. In: Proceedings of IFIP’83, North-Holland, pp 321–332
Jones CB (1983) Tentative steps toward a development method for interfering programs. Trans Program Lang Syst 5(4): 596–619
Jones CB (1990) Systematic software development using VDM, 2nd edn. Prentice Hall International, USA
Jones CB (1996) Accommodating interference in the formal design of concurrent object-based programs. Form Methods Syst Des 8(2): 105–122
Jones CB (2003) Wanted: a compositional approach to concurrency. In: McIver A, Morgan C (eds) Programming methodology. Springer, New York, pp 5–15
Jones CB (2007) Splitting atoms safely. Theor Comput Sci 375(1–3): 109–119
Jones CB (2010) The role of auxiliary variables in the formal development of concurrent programs. In: Jones CB, Roscoe AW, Wood K (eds) Reflections on the work of C.A.R. Hoare, vol 8. Springer, New York, pp 167–188
Jones CB (2012) Abstraction as a unifying link for formal approaches to concurrency. In: Eleftherakis G, Hinchey M, Holcombe M (eds) Software engineering and formal methods, vol 7504. Lecture notes in computer science, pp 1–15
Jones CB (2012) A specification for ACMs. Technical report CS-TR-1360, Newcastle University
Jones CB, Pierce KG (2008) Splitting atoms with rely/guarantee conditions coupled with data reification. In: ABZ2008, number 5238 in lecture notes in computer science. Springer, New York, pp 360–377
Jones CB, Pierce KG (2011) Elucidating concurrent algorithms via layers of abstraction and reification. Form Asp Comput 23(3): 289–306
Landin PJ (1966) The next 700 programming languages. Commun. ACM 9(3): 157–166
Liang H (2014) Refinement verification of concurrent programs and its applications. PhD thesis, USTC, China
Middelburg CA (1993) Logic and specification: extending VDM-SL for advanced formal specification. Chapman and Hall, London
Morris JM (1987) A theoretical basis for stepwise refinement and the programming calculus. Sci Comput Program 9(3): 287–306
Morgan CC (1994) Programming from specifications, 2nd edn. Prentice Hall, USA
Moszkowski B (1985) Executing temporal logic programs. In: Brookes SD, Roscoe AW, Winskel G (eds) Seminar on concurrency, vol 197 of LNCS. Springer, Berlin, pp 111–130
Owicki SS, Gries D (1976) An axiomatic proof technique for parallel programs I. Acta Inform 6: 319–340
O’Hearn PW (2007) Resources, concurrency and local reasoning. Theor Comput Sci 375(1–3): 271–307
Owicki S (1975) Axiomatic proof techniques for parallel programs. PhD thesis, Department of Computer Science, Cornell University
Parkinson M (2010) The next 700 separation logics. In: Leavens G, O’Hearn P, Rajamani S (eds) Verified software: theories, tools, experiments, vol 6217. Lecture notes in computer science. Springer, Berlin/Heidelberg, pp 169–182
Parkinson M, Bornat R, Calcagno C (2006) Variables as resource in Hoare logics. In: Proceedings of the 21st annual IEEE symposium on logic in computer science, pp 137–146
Prensa Nieto L (2001) Verification of parallel programs with the owicki-gries and rely-guarantee methods in Isabelle/HOL. PhD thesis, Institut für Informatic der Technischen Universitaet München
Prensa Nieto L (2003) The rely-guarantee method in Isabelle/HOL. In: Proceedings of ESOP 2003, vol 2618 of LNCS. Springer, New York
Reynolds JC (2000) Intuitionistic reasoning about shared mutable data structure. In: Davies J, Roscoe B, Woodcock J (eds) Millennial perspectives in computer science. Houndsmill, Hampshire, Palgrave, pp 303–321
Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of 17th LICS. IEEE, pp 55–74
Rodin (2008) Event-B and the Rodin platform. http://www.event-b.or.
Sangiorgi D (1999) Typed π-calculus at work: a correctness proof of Jones’s parallelisation transformation on concurrent objects. Theory Pract Obj Syst 5(1): 25–34
Svendsen K, Birkedal L (2014) Impredicative concurrent abstract predicates. In: Programming languages and systems. Springer, New York, pp 149–168
Simpson HR (1990) Four-slot fully asynchronous communication mechanism. Comput Dig Tech IEE Proc E 137(1): 17–30
Schellhorn G, Tofan B, Ernst G, Reif W (2011) Interleaved programs and rely-guarantee reasoning with ITL. In: Proceedings opf the eighteenth international symposium on temporal representation and reasoning (TIME), pp 99–106
Stølen K (1990) Development of parallel programs on shared data-structures. PhD thesis, Manchester University. Available as UMCS-91-1-1.
Turon A, Dreyer D, Birkedal L (2013) Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP’13. ACM, pp 377–390
Vafeiadis V (2007) Modular fine-grained concurrency verification. PhD thesis, University of Cambridge
Vafeiadis V, Parkinson M (2007) A marriage of rely/guarantee and separation logic. In: Caires L, Vasconcelos V (eds) CONCUR 2007— concurrency theory, vol 4703 of LNCS. Springer, NEw York, pp 256–271
von Wright J (2004) Towards a refinement algebra. Sci Comput Program 51: 23–45
Wickerson J (2013) Concurrent verification for sequential programs. PhD thesis, Cambridge
Wang S, Wang X (2010) Proving Simpson’s four-slot algorithm using ownership transfer. VERIFY Workshop, Edinburgh.
Author information
Authors and Affiliations
Corresponding author
Additional information
Communicated by George Eleftherakis, Mike Hinchey, and Michael Butler
Dedication: Wlad Turski 1938–2013
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution License which permits any use, distribution, and reproduction in any medium, provided the original author(s) and the source are credited.
About this article
Cite this article
Jones, C.B., Hayes, I.J. & Colvin, R.J. Balancing expressiveness in formal approaches to concurrency. Form Asp Comp 27, 475–497 (2015). https://doi.org/10.1007/s00165-014-0310-2
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-014-0310-2