Email Gateway (Aug 22 2022 at 18:59): Email Gateway (Aug 22 2022 at 18:59):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
on December 25 we got a Christmas submission that is now available to
everyone. The first new entry in 2019 is:
Formalization of Concurrent Revisions
by Roy Overbeek
Concurrent revisions is a concurrency control model developed by
Microsoft Research. It has many interesting properties that
distinguish it from other well-known models such as transactional
memory. One of these properties is determinacy:
programs written within the model always produce the same outcome,
independent of scheduling activity. The concurrent revisions model has
an operational semantics, with an informal proof of determinacy. This
document contains an Isabelle/HOL formalization of this semantics and
the proof of determinacy.
https://www.isa-afp.org/entries/Concurrent_Revisions.html
Happy New Year,
René
Last updated: Apr 26 2024 at 01:06 UTC