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

UNLV article access

Share

COinS