Verifying Channel Communication Correctness for a Multi-Core Cooperatively Scheduled Runtime Using CSP
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 model-checker to show that the generated Java code behaves like a generic synchronous, blocking, non-buffered one-to-one channel used previously to show the 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.
Mon 27 MayDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30
|Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks|
|Towards Sampling and Simulation-Based Analysis of Featured Weighted Automata|
|Verifying Channel Communication Correctness for a Multi-Core Cooperatively Scheduled Runtime Using CSP|
|A Generalized Program Verification Workflow Based on Loop Elimination and SA Form|