Communicating Cooperatively Scheduled Processes: On the Unlikelihood of Implementing a Pure CSP Channel
Kevin Chalmers, Jan Bækgaard Pedersen · Formal Aspects of Computing · 2025
This article presents the modelling of the ProcessJ cooperative runtime environment for the implementation of a CSP-inspired communication channel. We used the CSP tool FDR to verify the correctness of the ProcessJ runtime and primitives, demonstrating how we have overcome a limitation in the existing ProcessJ runtime to improve behaviour. However, our work has demonstrated a limitation when trying to claim a cooperatively-scheduled channel implementation meets the abstract specification of a CSP channel. Our conclusion is that without sufficient hardware to execute all processes at once, a channel implementation cannot fully meet its specification when considering the execution environment in which the channel must operate. We are assured that the ProcessJ channel works correctly, such as other implementations including JCSP and CSO, but we are not assured that modelling can use a pure CSP channel in place of a ProcesssJ channel or other implementation when undertaking modelling due to unintended prioritisation occurring when not enough resources are available for full concurrency. Our work has demonstrated the need to consider the execution environment as it may cause behavioural issues not detected when only modelling a system in the abstract.