Formal Aspects of Computing

, Volume 30, Issue 2, pp 239–277 | Cite as

The symbiosis of concurrency and verification: teaching and case studies

Open Access
Original Article
  • 42 Downloads

Abstract

Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS curriculum—no longer isolated, for example, as a support mechanism in a module on operating systems or reserved as an advanced discipline for later study. Formal verification of system properties is often considered a difficult subject area, requiring significant mathematical knowledge and generally restricted to smaller systems employing sequential logic only. This paper presents materials, methods and experiences of teaching concurrency and verification as a unified subject, as early as possible in the curriculum, so that they become fundamental elements of our software engineering tool kit—to be used together every day as a matter of course. Concurrency and verification should live in symbiosis. Verification is essential for concurrent systems as testing becomes especially inadequate in the face of complex non-deterministic (and, therefore, hard to repeat) behaviours. Concurrency should simplify the expression of most scales and forms of computer system by reflecting the concurrency of the worlds in which they operate (and, therefore, have to model); simplified expression leads to simplified reasoning and, hence, verification. Our approach lets these skills be developed without requiring students to be trained in the underlying formal mathematics. Instead, we build on the work of those who have engineered that necessary mathematics into the concurrency models we use (CSP, \({\pi}\) -calculus), the model checker (FDR) that lets us explore and verify those systems, and the programming languages/libraries (occam-\({\pi}\), Go, JCSP, ProcessJ) that let us design and build efficient executable systems within these models. This paper introduces a workflow methodology for the development and verification of concurrent systems; it also presents and reflects on two open-ended case studies, using this workflow, developed at the authors’ two universities. Concerns analysed include safety (don’t do bad things), liveness (do good things) and low probability deadlock (that testing fails to discover). The necessary technical background is given to make this paper self-contained and its work simple to reproduce and extend.

Keywords

Process-orientation Concurrency Deadlock Event ordering Liveness Verification Occam-\({\pi}\) CSP 

References

  1. ACM12.
    ACM/IEEE-CS Joint Task Force for Computing Curricula. Computer science curricula 2013, Ironman Draft (Version 0.8), November 2012. http://ai.stanford.edu/users/sahami/CS2013/. Accessed 01 Aug 2013
  2. BA10.
    Ben-Ari M (2010) A primer on model checking. ACM Inroads 1(1): 40–47CrossRefGoogle Scholar
  3. Bar95.
    Barrett G (1995) Model checking in practice: the T9000 virtual channel processor. IEEE Trans Softw Eng 21(2):69–78.  https://doi.org/10.1109/32.345823. Accessed 11 Dec 2017
  4. Bar05.
    Barnes FRM (2005) RMoX: an occam-\({\pi}\) operating-system, January 2005. http://www.frmb.org/rmox.html. Accessed 1 Dec 2017
  5. Bar06.
    Barnes Frederick RM (2006) Compiling CSP. In: Welch PH, Kerridge J, Barnes FRM (eds) Communicating process architectures 2006, vol 64, WoTUG-29 of concurrent systems engineering series. IOS Press, Amsterdam, pp 377–388. ISBN: 1-58603-671-8Google Scholar
  6. BKPS97.
    Buth B, Kouvaras M, Peleska J, Shi H (1997) Deadlock analysis for a fault-tolerant system. In: Proceedings of the 6th international conference on algebraic methodology and software technology (AMAST97), pp 60–75Google Scholar
  7. BPS99.
    Buth B, Peleska J, Shi H (1999) Combining methods for the livelock analysis of a fault-tolerant system. In: Proceedings of the 7th international conference on algebraic methodology and software technology (AMAST98), pp 124–139Google Scholar
  8. BR10.
    Barnes FRM, Ritson CG (2010) Checking process-oriented operating system behaviour using csp and refinement. ACM SIGOPS Oper Syst Rev 43(4): 45–49CrossRefGoogle Scholar
  9. Bro08.
    Brown Neil CC (2008) Communicating Haskell processes: composable explicit concurrency using monads. In: Welch PH, Stepney S, Polack FAC, Barnes FRM, McEwan AA, Stiles GS, Broenink JF, Sampson AT (eds) Communicating process architectures 2008, vol 66 of Concurrent systems engineering. WoTUG, IOS Press, Amsterdam, pp 67–83.Google Scholar
  10. Bro10a.
    Brown NCC (2010) C++CSP home page. Programming languages and systems research group, University of Kent. http://www.cs.kent.ac.uk/projects/ofa/c++csp/. Accessed 11 Dec 2017
  11. Bro10b.
    Brown NCC (2010) Communicating Haskell processes home page. Programming languages and systems research group, University of Kent. http://www.cs.kent.ac.uk/projects/ofa/chp/. Accessed 11 Dec 2017
  12. BW03.
    Brown NCC, Welch PH (2003) An introduction to the Kent C++CSP library. In: Broenink JF, Hilderink GH (eds) Communicating process architectures 2003, WoTUG-26, Concurrent systems engineering, ISSN 1383-7575. IOS Press, Amsterdam, pp 139–156. ISBN: 1-58603-381-6Google Scholar
  13. BW04.
    Barnes FRM, Welch PH (2004) Communicating mobile processes. In: East I, Martin J, Welch PH, Duce D, Green M (eds) Communicating process architectures 2004, vol 62, WoTUG-27 of Concurrent systems engineering series, ISSN 1383-7575. IOS Press, Amsterdam, pp 201–218. ISBN: 1-58603-458-8Google Scholar
  14. BWMW10.
    Barnes FRM, Welch PH, Moores J, Wood DC (2010) The KRoC home page. Programming languages and systems research group, University of Kent. http://www.cs.kent.ac.uk/projects/ofa/kroc/. Accessed 11 Dec 2017
  15. Cha16.
    Chalmers K (2016) Communicating process architectures in light of parallel design patterns and skeletons. In: Communicating process architectures 2015. Open Channel Publishing Ltd., pp 227–244. ISBN: 978-0-9565409-9-7Google Scholar
  16. Don94.
    Dongarra J (1994) MPI: a message passing interface standard. Int J Supercomput High Perform Comput 8: 165–184Google Scholar
  17. DT13.
    Danelutto M, Torquati M (2013) A RISC building block set for structured parallel programming. In: 21st euromicro international conference on parallel, distributed, and network-based processing, PDP 2013, Belfast, United Kingdom, February 27–March 1, 2013, pp 46–50Google Scholar
  18. GRABR14.
    Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2014) FDR3—a modern refinement checker for CSP. In: Tools and algorithms for the construction and analysis of systems 2014, vol LNCS 8413. Springer, BerlinGoogle Scholar
  19. GRABR16.
    Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2016) Failures divergences refinement (FDR) version 4Google Scholar
  20. GRS93.
    Goldsmith MH, Roscoe AW, Scott BGO (1993) Denotational semantics for occam2 (part 1). Transp Commun 1(2):65–91. Wiley, New York.Google Scholar
  21. GRS94.
    Goldsmith MH, Roscoe AW, Scott BGO (1994) Denotational semantics for occam2 (part 2). Transp Commun 2(1):25–67. Wiley, New York.Google Scholar
  22. HC02.
    Hall A, Chapman R (2002) Correctness by construction: developing a commercial secure system. IEEE Softw 19(1):18–25.  https://doi.org/10.1109/52.976937. Accessed 11 Dec 2017
  23. Hoa85.
    Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood CliffsGoogle Scholar
  24. Hol03.
    Holzmann G (2003) The spin model checker: primer and reference manual. Addison-Wesley Professional, ReadingGoogle Scholar
  25. JBV03.
    Jacobsen CL, Barnes FRM, Vinter B (2003) RMoX: a raw-metal occam experiment. In: Broenink JF, Hilderink GH (eds) Communicating process architectures 2003. IOS Press, Amsterdam, pp 269–288Google Scholar
  26. JJ04.
    Jacobsen CL, Jadud MC (2004) The transterpreter: a transputer interpreter. In: East IR, Duce D, Green M, Martin JMR, Welch PH (eds) Communicating process architectures 2004, vol 62, WoTUG-27 of Concurrent systems engineering series. IOS Press, Amsterdam, pp 99–106Google Scholar
  27. Low96.
    Lowe Gavin (1996) Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In: Tools and Algorithms for the Construction and Analysis of Systems, pages 147–166. Springer-VerlagGoogle Scholar
  28. Mil99.
    Milner R (1999) Communicating and mobile systems: the \({\pi}\) -calculus. Cambridge University Press, Cambridge, ISBN-10: 0521658691, ISBN-13: 9780521658690Google Scholar
  29. MS07.
    McEwan AA, Schneider S (2007) Modeling and analysis of the AMBA bus using CSP and B. In: McEwan AA (ed) Schneider S, Ifill W, Welch PH (eds) Communicating process architectures 2007, vol 65 WoTUG-30 of Concurrent systems engineering series. WoTUG, IOS Press, Amsterdam, pp 379 –398Google Scholar
  30. PW15.
    Pedersen JB, Welch PH (2017) The symbiosis of concurrency and formal verification: teaching and case studies. On-line Support Material. http://www.santaclausproblem.net/verification/. Accessed 1 Dec 2017
  31. RGG+95.
    Roscoe AW, Gardiner PHB, Goldsmith MH, Hulance JR, Jackson DM, Scattergood JB (1995) Hierarchical compression for model-checking CSP, or How to check \({10\hat20}\) dining philosophers for deadlock. In: Tools and algorithms for the construction and analysis of systems, vol LNCS 1019. Springer, BerlinGoogle Scholar
  32. RL10.
    Rustan K, Leino M (2010) Dafny: an automatic program verifier for functional correctness. In: 16th international conference on logic for programming artificial intelligence and reasoning, vol LNCS 6355. Springer, Berlin, pp 348–370Google Scholar
  33. Rob12.
    Pike R (2012) Go concurrency patterns, slides 5–8. http://talks.golang.org/2012/concurrency.slide. Accessed 1 Dec 2017
  34. Ros97.
    Roscoe A (1997) The theory and practise of concurrency. Prentice-Hall, Englewood CliffsGoogle Scholar
  35. Ros10.
    Roscoe AW (2010) Understanding concurrent systems. Springer, BerlinCrossRefMATHGoogle Scholar
  36. RSB12.
    Ritson CG, Sampson AT, Barnes FRM (2012) Multicore scheduling for lightweight communicating processes. Sci Comput Program 77(6): 727–740CrossRefGoogle Scholar
  37. RW07.
    Ritson CG, Welch PH (2007) A process-oriented architecture for complex system modelling. In: McEwan AA, Schneider S, Ifill W, Welch PH (eds) Communicating process architectures 2007, vol 65, WoTUG-30 of Concurrent systems engineering series. IOS Press, Amsterdam, pp 249–266. ISBN: 978-1-58603-767-3Google Scholar
  38. RW10.
    Ritson CG, Welch PH (2010) A process-oriented architecture for complex system modelling. Concurr Comput Pract Exp 22: 965–980CrossRefGoogle Scholar
  39. Sam07.
    Sampson AT (2007) Compiling occam to C with Tock—CPA 2007 Fringe. Systems Research Group, University of Kent. http://www.wotug.org/paperdb/send_file.php?num=217. Accessed 11 Dec 2017
  40. Sam08.
    Sampson AT (2008) Two-way protocols for occam-\({\pi}\). In: Welch PH, Stepney S, Polack FAC, Barnes FRM, McEwan AA, Stiles GS, Broenink JF, Sampson AT (eds) Communicating process architectures 2008, vol 66, WoTUG-31 of Concurrent systems engineering series. IOS Press, Amsterdam, pp 85–97Google Scholar
  41. Sam10.
    Sampson Adam T (2010) Process-oriented patterns for concurrent software engineering. PhD thesis, University of Kent, October 2010. http://offog.org/publications/ats-thesis.pdf. Accessed 11 Dec 2017
  42. SBR+10.
    Sampson AT, Brown NCC, Ritson CG, Jacobsen CL, Jadud MC, Simpson J (2010) Tock (translator from occam to C from Kent) home page. Systems Research Group, University of Kent, http://projects.cs.kent.ac.uk/projects/tock/trac/. Accessed 11 Dec 2017
  43. SD04.
    Schneider Steve, Delicata Rob (2004) Verifying security protocols: an application of CSP. In: Abdallah Ali E, Jones Cliff B, Sanders Jeff W (eds) Communicating sequential processes. The first 25 years, volume LNCS 3525, pp 243–263. Springer, BerlinGoogle Scholar
  44. SGS95.
    SGS-THOMSON Microelectronics Limited (1995) occam 2.1 reference manual. Prentice-Hall, Englewood CliffsGoogle Scholar
  45. SRJ+10.
    Sampson AT, Ritson CG, Jadud MC, Barnes FRM, Welch PH (2010) occam-\({\pi}\) home page. Programming Languages and Systems Research Group, University of Kent. http://occam-pi.org/. Accessed 11 Dec 2017
  46. Ste03.
    Stepney S (2003) CSP/FDR2 to Handel-C translation. Technical Report YCS-2002-357, Department of Computer Science, University of YorkGoogle Scholar
  47. SWT+07.
    Stepney S., Welch PH, Timmis J, Alexander C, Barnes FRM, Bates M, Polack FAC, Tyrrell A (2007) CoSMoS: complex systems modelling and simulation infrastructure, April 2007. EPSRC grants EP/E053505/1 and EP/E049419/1. http://www.cosmos-research.org/. Accessed 11 Dec 2017
  48. WB05a.
    Welch Peter H, Barnes Frederick RM (2005) Communicating Mobile processes: introducing occam-\({\pi}\). In: Abdallah Ali E, Jones Cliff B, Sanders Jeff W (eds) 25 years of CSP, volume 3525 of Lecture notes in computer science, pp 175–210. Springer, BerlinGoogle Scholar
  49. WB05b.
    Welch Peter H, Barnes Frederick RM (2005) Mobile barriers for occam-\({\pi}\) : semantics, implementation and application. In: Broenink Jan F, Roebbers Herman W, Sunter Johan PE, Welch Peter H Wood David C (eds) Communicating process architectures 2005, volume 63, WoTUG-28 of concurrent systems engineering series, pp 289–316. IOS Press, Amsterdam ISBN:1-58603-561-4Google Scholar
  50. WB08.
    Welch Peter H, Barnes Frederick RM (2008) A CSP model for mobile channels. In: Communicating process architectures 2008, volume 66, WoTUG-31 of concurrent systems engineering series, pp 17–33. IOS Press, Amsterdam. ISBN:978-1-58603-907-3Google Scholar
  51. WB11a.
    Welch P H, Brown N C C (2011) The JCSP (CSP for Java) Home Page, 2011. http://www.cs.kent.ac.uk/projects/ofa/jcsp/. Accessed 11 Dec 2017
  52. WB11b.
    Welch Peter H, Brown Neil CC (2011) Self-verifying dining philosophers. Presentation to IFIP Working Group 2.4, September 2011. https://www.cs.kent.ac.uk/research/groups/plas/wiki/IFIP_WG24. Accessed 11 Dec 2017
  53. WBM+07.
    Welch PH, Brown NCC, Moores J, Chalmers K, Sputh BHC (2007) Integrating and extending JCSP. In: McEwan Alistair A, Schneider S, Ifill W, Welch P (eds) Communicating process architectures 2007, volume 65 of concurrent systems engineering series, pp 349–370. IOS Press, Amsterdam. ISBN:978-1-58603-767-3Google Scholar
  54. WBM+10.
    Welch PH, Brown NCC, Moores J, Chalmers K, Sputh BHC (2010) Alting barriers: synchronisation with choice in Java using CSP. Concurr Comput Pract Exp 22: 1049–1062CrossRefGoogle Scholar
  55. Wel00.
    Welch Peter H (2000) Process oriented design for Java—concurrency for all. In: PDPTA 2000, vol 1, pp 51–57. CSREA Press. ISBN: 1-892512-52-1Google Scholar
  56. Wel13a.
    Welch Peter H (2013) Life of occam-Pi. In: Welch Peter H, Barnes Frederick RM, Broenink Jan F, Chalmers K, Pedersen Jan B, Sampson Adam T (eds) Communicating process architectures 2013, pp 293–318. Open Channel Publishing Ltd. ISBN:978-0-9565409-7-3. http://www.wotug.org/papers/CPA-2013/Welch13a/Welch13a.pdf. Accessed 11 Dec 2017
  57. Wel13b.
    Welch PH (2013) Concurrency design and practice, Course module. http://www.cs.kent.ac.uk/projects/ofa/sei-cmu/. Accessed 11 Dec 2017
  58. Wik13.
    Wikipedia (2013) XMOS XCore XS1. http://en.wikipedia.org/wiki/XCore. Accessed 11 Dec 2017
  59. WP10.
    Welch PH, Pedersen JB (2010) Santa Claus: formal analysis of a process-oriented solution. ACM Trans. Program. Lang. Syst. 32(4): 37CrossRefGoogle Scholar
  60. WPB+11.
    Welch Peter H, Pedersen Jan Baekgaard, Barnes Frederick R M, Ritson Carl G, Brown Neil CC (2011) Adding formal verification to occam-\({\pi}\). In: Communicating process architectures 2011, volume 68, WoTUG-33 of concurrent systems engineering series, pp 379–379. IOS Press, Amsterdam. ISBN:978-1-60750-773-4Google Scholar
  61. WPBR11.
    Welch Peter H, Pedersen Jan B, Barnes Frederick RM, Ritson Carl G (2011) Self-verifying concurrent programming. Presentation to IFIP Working Group 2.4, September 2011. https://www.cs.kent.ac.uk/research/groups/plas/wiki/IFIP_WG24. Accessed 11 Dec 2017
  62. WW96.
    Wood David C, Welch Peter H (1996) The kent retargetable occam compiler. In: O’Neill B (ed) Parallel processing developments, volume 47, WoTUG-19 of concurrent systems engineering series, pp 143–166, IOS Press, Amsterdam. ISBN:90-5199-261-0Google Scholar
  63. WWSK12.
    Welch PH, Wallnau K, Sampson AT, Klein M (2012) To boldly go: an occam-pi mission to engineer emergence. Nat Comput 11(3): 449–474MathSciNetCrossRefGoogle Scholar
  64. XMO13.
    XMOS Ltd. (2017) The xCORE difference. XMOS Ltd. http://www.xmos.com/products/silicon. Accessed 1 Dec 2017

Copyright information

© The Author(s) 2017

Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of Nevada Las VegasLas VegasUSA
  2. 2.School of ComputingUniversity of KentCanterburyUK

Personalised recommendations