From 238f8d009f6ac0d351db40e16bd39f4ab6650197 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dani=C3=ABl=20Louwrink?= <daniel.louwrink@gmail.com> Date: Wed, 6 May 2020 23:53:02 +0200 Subject: [PATCH] further updates to README.md --- README.md | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 8b598b9..aa14be3 100644 --- a/README.md +++ b/README.md @@ -13,8 +13,8 @@ In order to build, install the above dependencies and then run ## Logical relation The logical relation for type safety of the session type system is contained -in the directory [theories/logrel](theories/logrel). The files in this -directory contain the following parts of the paper: +in the directory [theories/logrel](theories/logrel). The logical relation is +defined across the following files: - [theories/logrel/model.v](theories/logrel/model.v): Definition of the notions of a semantic term type and a semantic session type in terms of @@ -46,9 +46,25 @@ directory contain the following parts of the paper: Semantic typing lemmas (typing rules) for the semantic term types. - [theories/logrel/session_typing_rules.v](theories/logrel/session.v): Semantic typing lemmas (typing rules) for the semantic session types. -- [theories/logrel/subtyping_rules.v): Subtyping rules for term types and +- [theories/logrel/subtyping_rules.v](theories/logrel/subtyping_rules.v): Subtyping rules for term types and session types. +An extension to the basic type system is given in +[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), which defines +mutexes as a type-safe abstraction. Mutexes are implemented using spin locks +and allow one to gain exclusive ownership of resource shared between multiple +threads. + +The logical relation is used to show that two example programs are semantically well-typed: +- [theories/examples/pair.v](theories/examples/pair.v): This program performs + two sequential receives and stores the results in a pair. It is shown to be + semantically well-typed by applying the semantic typing rules. +- [theories/examples/double.v](theories/examples/double.v): This program + performs two ``racy'' parallel receives on the same channel from two + different threads, using locks to allow the channel to be shared. This + program cannot be shown to be well-typed using the semantic typing rules. + Therefore, a manual proof of the well-typedness is given. + ## Theory of Actris The theory of Actris (semantics of channels, the model, and the proof rules) -- GitLab