Wortelboer, Sjors (2024) λ-lock encoding to π-calculus. Master's Internship Report, Computing Science.
|
Text
mCS2024WortelboerS.pdf Download (339kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming.pdf Restricted to Registered users only Download (134kB) |
Abstract
λlock, by Jacobs et al [3], is a deadlock-free functional language that introduces concurrent processing with resource sharing through locks. CLASS, by Rocha [4], achieves the same through an extension of a linear π-calculus called μCLL. This project develops an encoding from λlock to CLASS. The necessity comes from the fact that λlock is not confluent and has a degree of non-determinism that makes it hard to verify the outcomes of any program. CLASS also captures the non-deterministic behaviour of locks (called cells) but does not make a choice and hence preserves the property of confluence. Any reduction in CLASS thus captures all possible outcomes. To allow the development of the encoding CLASS is extended into CLASS+, which captures the ownership property of λlock and the behaviour of discarding locks while preserving the stored values.
| Item Type: | Thesis (Master's Internship Report) |
|---|---|
| Supervisor name: | Perez Parra, J.A. and Frumin, D. |
| Degree programme: | Computing Science |
| Thesis type: | Master's Internship Report |
| Language: | English |
| Date Deposited: | 26 Jul 2024 14:17 |
| Last Modified: | 26 Jul 2024 14:17 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/33715 |
Actions (login required)
 |
View Item |