Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908590881636352 |
|---|---|
| author | Pedersen, Jan Chalmers, Kevin |
| author_facet | Pedersen, Jan Chalmers, Kevin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_11751 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language Pedersen, Jan Chalmers, Kevin Programming Languages 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. |
| title | Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2510.11751 |