Nettsider med emneord «concurrency»

Publisert 24. sep. 2018 17:31
Publisert 25. sep. 2017 21:01

The presentation by Daniel Fava at the Doctoral Symposium of the 13th International  integrated Formal Methods (iFM 2017) won the award for  the symposium's best presentation (shared with a second winner). The presentation covers joint work with Martin Steffen, Volker Stolz, and Stian Valle, about   ``An Operational Semantics for a Weak Memory Model with Buffered Writes, Message Passing, and Goroutines''.

 

Publisert 25. aug. 2017 09:37

This is a general topic regarding the foundations of programming languages and their semantics. Here the student can choose various topics to focus on, depending on the interest, which we find out together through discussions.

One can do various kinds of MSc theses, starting from just programming a simple tool related to some variant of Keene algebra, or a literature study, or doing modelling of real systems, or using existing tools for Kleene algebras like proof assistants, or doing mathematical proofs.

Ask for discussions with one of the supervisors, for more information or variations of the project. See also general concerns.

Publisert 5. nov. 2016 09:46

Memory models as a part of programming language specifications have become increasingly popular the last two decades. They describe how the values that are obtained by reads are related to the values that are written by writes. To properly define this has proven particularly difficult for programming languages that allows for shared variables between multiple processes. In this thesis we formalize parts of the memory model specified by the Go language by making a structural operational semantics for it. We further use this semantics to prove that programs that are data race free will run under this semantics as they would under a strong memory model.

Publisert 23. sep. 2016 13:45

by Lars Tveito

Real-time collaboration allows multiple users to view and edit a document simultaneously over a network. In this thesis, we develop a new protocol, called Shared Buffer, which enables real-time collaboration in existing editors. Shared Buffer leverages a client-server architecture and minimizes the implementation effort of the client-side algorithm. It achieves this without degrading the responsiveness of the editor.

The greatest challenge of a real-time collaborative system is ensuring consistency between the distributed copies of the document. We chose eventual consistency as the consistency model, which essentially states that if all users stop typing, then eventually they will look at the same document.

We apply a formal verification technique called model checking, using it as a tool to validate the protocol. The behavior of the system is formally specified in Maude, a language based on equational and rewriting logic. Linear Temporal Logic (LTL) is used to formalize the consistency model. Using the Maude LTL model checker, we have verified that the system exhibits eventual consistency for a limited number of clients and operations.

A Shared Buffer server has been implemented in Clojure, a modern functional language with strong support for concurrency. Client implementations have been developed as an extension for Emacs, a widely used text editor, and as a library for the Python programming language.

Publisert 4. des. 2015 12:32
Publisert 16. aug. 2015 21:30

"Modelling Tools and Programming languages for Internet of Things"

Publisert 16. aug. 2015 21:26

"Modelling Tools and Programming languages for Internet of Things"

Publisert 13. jan. 2015 08:27
Publisert 1. des. 2014 08:23
Publisert 22. sep. 2014 16:14
Publisert 3. mars 2011 20:37
Publisert 11. feb. 2011 09:51

The Reliable Systems group PSY (formerly PMA) teaches the following courses:

Publisert 9. nov. 2010 10:47
Publisert 4. nov. 2010 14:19
Publisert 4. nov. 2010 14:12
Publisert 4. nov. 2010 13:50
Publisert 4. nov. 2010 13:50