Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language

TL;DR

The paper tackles correctness of shared channels in a cooperatively scheduled ProcessJ runtime by building CSP specifications and translating the runtime implementation into CSP models verified with FDR. It demonstrates that the ProcessJ shared-channel implementations are correct relative to the CSP spec when sufficient scheduling resources are available, and provides an algebraic proof that the generic shared-channel spec matches a CSP channel. A key finding is that the number of schedulers relative to the number of active processes governs refinement in both directions, underscoring the need to model the execution environment for accurate verification. The work advances the verification of runtime concurrency by integrating formal CSP models with an actual cooperative scheduler, informing both design and analysis of concurrent runtimes in real-world settings.

Abstract

Correct concurrent behaviour is important in understanding how components will act within certain conditions. In this work. we analyse the behaviour of shared communicating channels within a coorporatively scheduled runtime. We use the refinement checking and modelling tool FDR to develop both specifications of how such shared channels should behave and models of the implementations of these channels in the cooperatively scheduled language ProcessJ. Our results demonstrate that although we can certainly implement the correct behaviour of such channels, the outcome is dependant on having adequate resources available to execute all processes involved. We conclude that modelling the runtime environment of concurrent components is necessary to ensure components behave as specified in the real world.

Figures (7)

• Figure 1: The $N\_SCHEDULER\_SYSTEM$ network.
• Figure 2: Example ProcessJ shared reading (one-to-many) and shared writing (many-to-one) channels.
• Figure 3: Four interactions of channels.
• Figure 4: The MANY_TO_ONE_CHANNEL process.
• Figure 5: The RESTRICTED_PJ_MANY_TO_ONE_CHAN_SYSTEM process network.