Verifying Channel Communication Correctness for a Multi-core Cooperatively Scheduled Runtime Using CSP
Jan Bækgaard Pedersen, Kevin Chalmers · 2019
In this paper we use the process algebra CSP and the formal model-checker FDR to show that the implementation of one-to-one channel communication in the process-oriented language ProcessJ is correct. ProcessJ is a new process-oriented language with Java-like syntax and CSP-based communication using synchronous channels. ProcessJ allows for hundreds of millions of processes to be executed on a single processor core. ProcessJ generates Java code which eventually runs concurrently on the JVM using a cooperative scheduler. We use the translation from the ProcessJ code generator to translate ProcessJ to Java and further into CSP. We then utilize the FDR modelchecker to show that the generated Java code behaves like a generic synchronous, blocking, non-buffered one-to-one channel used previously to show correctness of channel communication in JCSP - a Java library that supports JVM thread-based concurrency. Finally, we highlight a lesson from verifying our behaviour using FDR - the ability to simplify our approach and show the implementation still meets our specification.