Verifying Channel Communication Correctness for a Multi-core Cooperatively Scheduled Runtime Using CSP
Document Type
Conference Proceeding
Publication Date
5-27-2019
Publication Title
2019 IEEE/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE)
Publisher
Institute of Electrical and Electronics Engineers
Publisher Location
Montreal, Canada
First page number:
65
Last page number:
74
Abstract
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.
Disciplines
Computer Sciences
Language
English
Repository Citation
Pedersen, J.,
Chalmers, K.
(2019).
Verifying Channel Communication Correctness for a Multi-core Cooperatively Scheduled Runtime Using CSP.
2019 IEEE/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE)
65-74.
Montreal, Canada: Institute of Electrical and Electronics Engineers.
http://dx.doi.org/10.1109/FormaliSE.2019.00016