Cristin-prosjekt-ID: 2531874
Sist endret: 27. januar 2022, 18:56

Cristin-prosjekt-ID: 2531874
Sist endret: 27. januar 2022, 18:56
Prosjekt

Synchronous Languages meet Asynchronous Semantics

prosjektleder

Ka I Pun
ved Institutt for datateknologi, elektroteknologi og realfag ved Høgskulen på Vestlandet

prosjekteier / koordinerende forskningsansvarlig enhet

  • Høgskulen på Vestlandet

Finansiering

  • Norges forskningsråd
    Prosjektkode: 309794

Tidsramme

Aktivt
Start: 1. januar 2020 Slutt: 31. desember 2022

Beskrivelse Beskrivelse

Tittel

Synchronous Languages meet Asynchronous Semantics

Vitenskapelig sammendrag

In the world of concurrent programs, futures are often used to synchronise asynchronous operations. In general, futures can be categorised as either implicit or explicit. With implicit futures, it is in general not possible to decide if a variable holds a future value or a concrete value in program codes, and the synchronisation points are implicit and hidden from the programmers. On the contrary, explicit futures use a future type to explicitly indicate the use of a future in the program, and the synchronisation points are explicit and controlled by the programmers. It is observed that the synchronisation of implicit futures and explicit futures is based on dataflow and control-flow, respectively.

This project plans to lift the integration of dataflow and control-flow futures to the level of programming language semantics by developing a formal specification format to allow a seamless transition from control-flow driven programming to dataflow oriented. Such a specification can be developed in terms of a formalisation based on symbolic trace semantics. Symbolic trace semantics is more expressive than traditional state-based semantics; it relies on symbolic traces and is thus more convenient to reason about the behaviour of programs in a symbolic and compositional way.

It is challenging to achieve such an integration: In practice, we need a symbolic trace semantics in which synchronisation triggers an unbounded number of communication events. In the trace, we will have the choice between showing a single synchronisation step, which facilitates reasoning about the program but is more difficult to write, or exposing intermediate steps which bring complementary properties: it is more precise but does not correspond to the programmer's perspective. This project will therefore focus on these chagllenges, and a successful result of this project will form a basis for the unification of futures, asynchronous actors, and synchronous languages.

prosjektdeltakere

prosjektleder

Ka I Pun

  • Tilknyttet:
    Prosjektleder
    ved Institutt for datateknologi, elektroteknologi og realfag ved Høgskulen på Vestlandet
1 - 1 av 1

Resultater Resultater

Active Objects with Deterministic Behavior.

Henrio, Ludovic; Johnsen, Einar Broch; Pun, Ka I. 2020, Lecture Notes in Computer Science (LNCS). UIO, UDL, HVLVitenskapelig artikkel
1 - 1 av 1