Advertisement

Encoding Fairness in a Synchronous Concurrent Program Algebra

  • Ian J. Hayes
  • Larissa A. Meinicke
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

Concurrent program refinement algebra provides a suitable basis for supporting mechanised reasoning about shared-memory concurrent programs in a compositional manner, for example, it supports the rely/guarantee approach of Jones. The algebra makes use of a synchronous parallel operator motivated by Aczel’s trace model of concurrency and with similarities to Milner’s SCCS. This paper looks at defining a form of fairness within the program algebra. The encoding allows one to reason about the fair execution of a single process in isolation as well as define fair-parallel in terms of a base parallel operator, of which no fairness properties are assumed. An algebraic theory to support fairness and fair-parallel is developed.

Notes

Acknowledgements

This research was supported Australian Research Council Discovery Grant DP130102901. Thanks are due to Robert Colvin, Rob Van Glabbeek, Peter Höfner, Cliff Jones, and Kirsten Winter, for feedback on ideas presented here. This research has benefited greatly from feedback members of IFIP Working Group 2.3 on Programming Methodology, in particular, at the meeting in Villebrumier.

References

  1. 1.
    Aarts, C., Backhouse, R., Boiten, E., Doombos, H., van Gasteren, N., van Geldrop, R., Hoogendijk, P., Voermans, E., van der Woude, J.: Fixed-point calculus. Inf. Process. Lett. 53, 131–136 (1995)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Aczel, P.H.G.: On an inference rule for parallel composition (1983). Private communication to Cliff Jones. http://homepages.cs.ncl.ac.uk/cliff.jones/publications/MSs/PHGA-traces.pdf
  3. 3.
    Colvin, R.J., Hayes, I.J., Meinicke, L.A.: Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects Comput. 29, 853–875 (2016)MathSciNetCrossRefGoogle Scholar
  4. 4.
    de Boer, F.S., Hannemann, U., de Roever, W.-P.: Formal justification of the rely-guarantee paradigm for shared-variable concurrency: a semantic approach. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1245–1265. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48118-4_16CrossRefzbMATHGoogle Scholar
  5. 5.
    de Roever, W.-P.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  6. 6.
    Hayes, I.J.: Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects Comput. 28(6), 1057–1078 (2016)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Hayes, I.J., Meinicke, L.A.: Encoding fairness in a synchronous concurrent program algebra: extended version with proofs. arXiv:1805.01681 [cs.LO] (2018)
  8. 8.
    Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A.: An algebra of synchronous atomic steps. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 352–369. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-48989-6_22CrossRefGoogle Scholar
  9. 9.
    Hayes, I.J., Meinicke, L.A., Winter, K., Colvin, R.J.: A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Accepted for publication in Formal Aspects of Computing (2018)Google Scholar
  10. 10.
    Jones, C.B.: Development methods for computer programs including a notion of interference. Ph.D. thesis, Oxford University, June 1981. Available as: Oxford University Computing Laboratory (now Computer Science) Technical Monograph PRG-25Google Scholar
  11. 11.
    Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP 1983, pp. 321–332. North-Holland (1983)Google Scholar
  12. 12.
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM ToPLaS 5(4), 596–619 (1983)CrossRefGoogle Scholar
  13. 13.
    Lehmann, D., Pnueli, A., Stavi, J.: Impartiality, justice and fairness: the ethics of concurrent termination. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 264–277. Springer, Heidelberg (1981).  https://doi.org/10.1007/3-540-10843-2_22CrossRefGoogle Scholar
  14. 14.
    Milner, A.J.R.G.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  15. 15.
    Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25(3), 267–310 (1983)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Park, D.: On the semantics of fair parallelism. In: Bjøorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 504–526. Springer, Heidelberg (1980).  https://doi.org/10.1007/3-540-10007-5_47CrossRefGoogle Scholar
  17. 17.
    van Glabbeek, R.J.: Ensuring liveness properties of distributed systems (a research agenda). Technical report, NICTA, March 2016. Position paperGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.The University of QueenslandBrisbaneAustralia

Personalised recommendations