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

Basic Information

• Paper ID: 2510.11751
• Title: Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language
• Authors: Jan Pedersen (University of Nevada Las Vegas), Kevin Chalmers (Ravensbourne University)
• Classification: cs.PL (Programming Languages)
• Publication Date: October 12, 2025 (arXiv preprint)
• Paper Link: https://arxiv.org/abs/2510.11751

Abstract

This paper analyzes the behavior of shared communication channels in a cooperatively scheduled runtime environment. The research develops specifications for shared channel behavior and models of channel implementations in the ProcessJ language using the formal verification tool FDR. The results demonstrate that while correct channel behavior can be implemented, the results depend on having sufficient resources to execute all relevant processes. The study concludes that modeling the runtime environment of concurrent components is necessary to ensure that components behave according to specification in real-world scenarios.

Research Background and Motivation

Problem Context

1. Importance of Concurrent Software Correctness: The correct behavior of concurrent systems is crucial for understanding how components execute under specific conditions. While traditional testing methods are widely used, they may fail to discover all potential concurrency errors.
2. Necessity of Formal Verification: The authors use Mars rover software as an example, demonstrating that a simple deadlock error might require waiting 80 million seconds (over 90 days) to have a 50% probability of being discovered through testing, whereas formal verification using CSP and FDR can identify such errors immediately.
3. Challenges in Runtime System Verification: Since many programs are built on top of programming language runtime systems, ensuring that runtime systems are error-free and behave according to specification becomes critically important.

Limitations of Existing Approaches

1. Neglecting Execution Environments: Traditional channel system verification methods do not model runtime systems, execution systems, hardware, and other factors, assuming that ready events remain available until scheduled.
2. Resource Scarcity Assumptions: Standard modeling methods assume events can occur immediately, meaning resources are available when executing events. However, this extreme assumption does not hold in practice.
3. Impact of Scheduling Environments: Processes must wait at the end of the ready queue to be scheduled, and their events are not immediately available. However, traditional methods do not account for this situation.

Research Motivation

ProcessJ is a process-oriented programming language based on CSP semantics that employs cooperative scheduling and runs on the JVM. This paper aims to verify the correctness of shared channel implementations in the ProcessJ runtime, particularly focusing on how the scheduling environment affects channel behavior.

Core Contributions

1. Verified the Correctness of ProcessJ Shared Channel Implementations: Demonstrated that ProcessJ shared channel implementations using the existing cooperative scheduler are correct, verified through CSP translation and refinement checking against a generic shared channel model.
2. Developed Extended Algebraic Proofs for Shared Channel Specifications: Provided formal proofs that shared channel specifications indeed behave as CSP shared channels.
3. Further Demonstrated the Relationship Between Resources and Active Processes: Reiterated the relationship between available resources and the number of active processes for satisfying specifications, proving that the number of available schedulers must be equal to or greater than the number of processes in the system to achieve refinement in both directions between specification and model.

Methodology Details

Task Definition

The core task of this paper is to verify the correctness of shared channel implementations in the ProcessJ language. Specifically, it includes:

• Input: Java implementation code of ProcessJ shared channels and CSP specifications
• Output: Verification results proving whether implementations conform to specifications
• Constraints: Considering resource limitations in a cooperatively scheduled environment

Model Architecture

1. CSP Modeling Framework

Using Communicating Sequential Processes (CSP) as the formal modeling language:

• Processes: Abstract components defined by the events they execute
• Events: Atomic, synchronous, instantaneous communication operations
• Channels: Media for inter-process communication

2. Scheduling System Modeling

SCHEDULER = 
  rqdequeue?p → -- dequeue a process
  run.p → -- execute it
  yield.p → -- await yield
  SCHEDULER -- recursion

SCHEDULE_MANAGER = 
  schedule?pid → -- await scheduling event
  rqenqueue!pid → -- place process in run queue
  SCHEDULE_MANAGER -- recursion

3. Process Metadata Modeling

Each process requires monitors, running flags, and ready flags:

PROCESS(p) = 
  VARIABLE(ready.p, true)
  ||| VARIABLE(running.p, false)
  ||| MONITOR(claim_process.p, release_process.p)

4. Shared Channel Modeling

• Many-to-One Channels: Multiple writer processes, one reader process
• One-to-Many Channels: One writer process, multiple reader processes
• Many-to-Many Channels: Multiple writer processes, multiple reader processes

Technical Innovations

1. Verification Method Considering Scheduling Environment

Unlike traditional methods, this paper explicitly models the cooperative scheduler during verification, enabling discovery of issues that only appear under specific scheduling conditions.

2. Refinement Checking Under Resource Constraints

By varying the number of schedulers, the study examined how system behavior changes under different resource configurations, revealing the relationship between resource sufficiency and correctness.

3. Bidirectional Translation from Implementation to Specification

• ProcessJ code → Java code → CSP model
• Establishes a complete translation chain ensuring verification result reliability

Experimental Setup

Verification Tools

• FDR (Failures-Divergences Refinement): CSP refinement checking tool
• CSPM: Machine-readable CSP version

Verification Models

Three semantic models are used for analysis:

1. Traces Model: Based on external observable behavior
2. Stable Failures Model: Handles events that processes may refuse
3. Failures-Divergences Model: Handles potential livelock scenarios

Test Configurations

• Process Configurations: Various combinations of 1-2 writer processes and 1-3 reader processes
• Scheduler Numbers: 1 to 4 schedulers
• Channel Types: One-to-many, many-to-one, many-to-many shared channels

Experimental Results

Main Results

| Channel Type | Process Configuration | Total Processes | Scheduler Count ||||| |--------------|----------------------|-----------------|--|--|--|--| | | | | 1| 2| 3| 4| | One-to-Many | 1 writer-2 readers | 3 | T| T| F| F| | One-to-Many | 1 writer-3 readers | 4 | T| T| T| F| | Many-to-One | 2 writers-1 reader | 3 | T| T| F| F| | Many-to-One | 3 writers-1 reader | 4 | T| T| T| F| | Many-to-Many | 2 writers-2 readers | 4 | T| T| T| F|

Symbol Legend:

• T = Passes traces refinement check
• F = Passes failures refinement check
• ✗ = Refinement check fails

Key Findings

1. Resource Sufficiency Theorem: When the number of schedulers equals or exceeds the total number of processes, refinement can be achieved in both directions of the failures model.
2. Impact of Resource Insufficiency:
   • With insufficient schedulers, only traces refinement rather than failures refinement can be achieved
   • This does not mean the system will deadlock, but rather that certain traces are no longer realizable
3. Impact of Scheduling Queue: The run queue imposes a natural ordering on processes. When schedulers are insufficient, the acceptance sets of certain processes are not included in the overall acceptance set of the system.

Related Work

Formal Verification Domain

• CSO and JCSP Verification: Previous work verified runtime systems of other languages but neglected execution environments
• SPIN Model Checking: Other systems use similar verification methods but typically assume preemptive scheduling

Cooperative Scheduling Research

• occam-π Scheduler: The ProcessJ scheduler is similar to occam-π's multiprocessor cooperative scheduler
• Async/Await Patterns: Cooperative multitasking is increasingly popular in JavaScript, Python, C++, and Rust

Advantages of This Work

1. First to Consider Scheduling Environment: Explicitly models cooperative scheduler in verification
2. Discovers Scheduling-Related Issues: Can detect livelocks and other issues that only appear under specific scheduling conditions
3. Resource-Aware Verification: Quantifies the relationship between resource requirements and correctness

Conclusions and Discussion

Main Conclusions

1. Implementation Correctness: ProcessJ's shared channel implementation is correct when sufficient schedulers are available.
2. Resource Dependency: Correct behavior depends on having sufficient scheduling resources to execute all relevant processes.
3. Necessity of Modeling: Modeling the runtime environment is necessary to ensure that components behave according to specification in real-world scenarios.

Limitations

1. Lock Usage: The current implementation makes extensive use of locks/monitors, which may impact concurrency and performance.
2. Scheduler Requirements: Requiring a number of schedulers equal to the number of processes may be impractical in real applications.
3. Verification Complexity: The state space of verification grows rapidly as the number of processes increases.

Future Directions

1. Lock-Free Implementations:
   • Replace locks with atomic variables
   • Implement wait-free queue structures
   • Develop CSP models supporting compare-and-swap operations
2. Specification Simplification:
   • Develop lightweight CSP model construction methods
   • Study ProcessJ behavior under different scheduling conditions
3. Scheduler Optimization:
   • Investigate whether failures refinement can be achieved with fewer schedulers than processes
   • Analyze scheduler requirements for different programs

In-Depth Evaluation

Strengths

1. Methodological Innovation:
   • First to consider cooperative scheduling environment in formal verification
   • Establishes a complete verification chain from implementation to specification
2. Theoretical Contributions:
   • Provides rigorous algebraic proofs for shared channel specifications
   • Quantifies the relationship between resource requirements and correctness
3. Practical Value:
   • Verifies the correctness of actual runtime systems
   • Provides verification methods for other cooperatively scheduled systems
4. Experimental Sufficiency:
   • Tests multiple channel configurations and scheduler numbers
   • Uses rigorous CSP/FDR verification methods

Weaknesses

1. Scalability Issues:
   • Verification complexity grows exponentially with process count
   • Requiring many schedulers may limit practical applications
2. Insufficient Performance Considerations:
   • Extensive lock usage may impact system performance
   • Verification overhead not thoroughly discussed
3. Limited Scope of Applicability:
   • Primarily targets ProcessJ language
   • Applicability to other cooperatively scheduled systems requires further verification

Impact

1. Academic Contribution:
   • Provides new verification insights for programming languages and formal methods
   • Advances development of verification methods considering execution environments
2. Practical Value:
   • Improves reliability of ProcessJ runtime
   • Provides reference for runtime verification of other languages
3. Reproducibility:
   • Provides complete CSP code and test scripts
   • Verification process and results can be independently reproduced

Applicable Scenarios

1. Process-Oriented Programming Languages: Particularly suitable for runtime verification of CSP-based languages
2. Cooperative Scheduling Systems: Applicable to other concurrent systems using cooperative scheduling
3. Critical System Development: Suitable for concurrent system development with extremely high correctness requirements

References

This paper cites 51 related references, primarily including:

1. CSP Foundational Theory: Hoare's classical CSP works and related theory
2. Formal Verification Tools: FDR tools and related verification methods
3. Concurrent Programming Languages: Related research on JCSP, occam-π, Go, Erlang, and other languages
4. Scheduling Algorithms: Related work on mutual exclusion and concurrent algorithms
5. Authors' Previous Work: Series of research on ProcessJ runtime verification

Summary: This paper makes important contributions to the formal verification domain, particularly in verifying concurrent systems considering execution environments. While some limitations exist, its methods and findings have significant value for improving the reliability of concurrent systems.