|Title:||Concurrency, Intuition and Formal Verification: Yes, We Can! (Ben-Ari's Twin-Process Conundrum)|
|Conference:||Communicating Process Architectures 2017|
Jan Bækgaard Pedersena, Peter H. Welchb
(a) Department of Computer Science, University of Nevada Las Vegas
(b) School of Computing, University of Kent
Not only can (and should) concurrency be introduced early in the undergraduate CS curriculum – but mechanisms for its formal analysis and verification can be presented that are intuitive, effective and easy to learn and apply. Further, this can be done without requiring students to be trained in the underlying formal mathematics. Instead, we stand on the shoulders of giants who have engineered the necessary mathematics into the concurrency models we use (CSP, π-calculus), the programming languages/libraries (occam-π, JCSP, Process-J) that let us design and build efficient executable systems within these models, and the model checker (FDR3) that lets us explore and verify those systems. All we require from our students are a love of the subject, a flair for programming and some time and effort. This talk presents some experience over the past ten years that lets us make these claims.
The reason for the "should" in the first sentence of this abstract is as follows. Multi-core architectures are now standard, with the number of cores per processor growing each year. Multi-processor networks are inescapable for super-computing problems and many (most?) forms of embedded computer platform. Engineers (and students) cannot avoid concurrent reasoning when dealing with these devices – avoidance leads to many bad things. Verification of this concurrent reasoning is mostly set aside (as it has generally been for sequential reasoning, we admit). A significant amount of professional development time and money is spent instead on testing software. However, testing and debugging concurrent programs is even more difficult than testing and debugging sequential programs: common faults are intermittent and not reproducible on demand. If the concurrency pattern is beyond the embarrassingly parallel (i.e., the processes need to engage with each other) and we have made some mistakes in design or coding, testing may never see these faults ... and our system will eventually fail in service (on Mars, for instance). So, we need to verify. Now, just as we need tools (e.g. programming languages) to produce executable systems, we need tools (e.g. model checkers) to produce verified systems. Language and model checker pairs need to live to the same concurrency model.
We present "Ben-Ari's Conundrum" as an example of how to follow the workflow and demonstrate its usability and wins. We invite the audience to have a go at predicting the solution to the conundrum in advance. The problem is something that may seem relatively straightforward, but turns out to not be quite as simple as it looks. Significant aspects of behaviour were overlooked by Ben-Ari for several years, until one of his students observed something that should not have happened.