Seminars

  • Verify me if you can: Supervisors, Actors and Session Types

    Rumyana Neykova

    Imperial College London

    Abstract: 

    Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing communication safety of the participating entities. The usage of multiple roles allows safe cooperative interconcurrency in a single actor. We present the design of our session actor library in Python, which is evaluate by implementing twelve use cases from an actor benchmark suit. Benchmarks demonstrate that the runtime checks induce negligible overhead. We also present a recent work incorporating the session actors model into Erlang, where session types are used for faster error recovery on top of Erlang supervision trees.

    Where: 
    6.3.5
    When: 
    Wednesday, March 11 2015
    Time: 
    11:00
  • Mignis: A semantic based tool for firewall configuration

    Pedro Adão

    IST, University of Lisbon

    Abstract: 

    The management and specification of access control rules that enforce a given policy is a non-trivial, complex, and time consuming task. The goal of Mignis is to simplify this task both at specification and verification levels. We start by proposing a formal model of Netfilter, a firewall system integrated in the Linux kernel, where we abstract the concepts of chains, rules, and packets existent in Netfilter configurations, and give a semantics that mimics packet filtering and address translation. We then introduce a simple but powerful language that allows one to specify firewall configurations that are unaffected by the relative ordering of rules, and that does not depend on the underlying Netfilter chains. We give a semantics for this language and show that it can be translated into our Netfilter abstraction. We finally present Mignis, a publicly available tool that translates abstract firewall specifications into real Netfilter configurations.
    This is joint work with Claudio Bozzato, Gian-Luca Dei Rossi, Riccardo Focardi and Flaminia Luccio.

    Where: 
    6.3.5
    When: 
    Wednesday, January 7 2015
    Time: 
    11:30
  • Multiparty Sessions based on Proof Nets

    Dimitris Mostrous

    FCUL

    Abstract: 

    We interpret Linear Logic Proofs (Proof Nets) in a process language based on Solos calculus. The language includes a synchronisation mechanism, obtained by a conservative extension of the logic, that enables to define non-deterministic behaviours and multiparty sessions. Typed terms are strongly normalising, which is the first result of this kind for multiparty interactions.
    From the programming perspective, our proposal provides a logically founded approach to multiparty sessions; from the logic perspective, our contribution fits the challenging theme of a "Curry-Howard" correspondence for concurrency.

    This work was presented in PLACES 2014, and is available at http://www.di.fc.ul.pt/~dimitris/Multiparty_Nets_PLACES14.pdf

    Where: 
    6.3.38
    When: 
    Wednesday, June 25 2014
    Time: 
    13:30
  • Communication contracts for MPI-like languages

    Vasco T. Vasconcelos

    FCUL

    Abstract: 

    We present a notion of dependent types that abstracts the communication part of Message Passing Interface (MPI) -like programs. Such types are naturally equipped with a reduction relation and we show that types do not get stuck. We then move to describe a core programming language whose terms inhabit types. We show that programs do not get stuck, crucially relying on the homonymous result for types. We finally describe a framework for checking the conformance of C+MPI programs against types, relying on the VCC tool.
    [Joint work with Francisco Martins, Eduardo Marques, Nobuko Yoshida, Nicholas Ng]

    Where: 
    6.3.5
    When: 
    Tuesday, May 20 2014
    Time: 
    16:30
  • Mutually testing processes

    Giovanni Bernardi

    FCUL

    Abstract: 

    In the standard testing theory of DeNicola-Hennessy one process is considered to be a refinement of another if every test guaranteed by the former is also guaranteed by the latter. In the domain of web services this has been recast, with processes viewed as servers and tests as clients. In this way the standard refinement preorder between servers is determined by their ability to satisfy clients.

    But in this setting there is also a natural refinement preorder between clients, determined by their ability to be satisfied by servers. In more general settings where there is no distinction between clients and servers, but all processes are peers, there is a further refinement preorder based on the mutual satisfaction of peers.

    In this talk we explain the notions sufficient to give uniform behavioural characterisations of all three preorders. We focusing in particular on the characterisation of the client preorder.

    Where: 
    6.3.38
    When: 
    Wednesday, March 26 2014
    Time: 
    10:00
  • Affine Sessions

    Dimitris Mostrous

    FCUL

    Abstract: 

    Session types describe the structure of protocols from the point of view of each participating channel. In particular, the types describe the type of communicated values, and also the dynamic alternation of input and output actions on the same channel, by which a protocol can be statically verified. Crucial to any term language with session types is the notion of linearity, which guarantees that channels exhibit exactly the behaviour prescribed by their type. We relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck.

    Where: 
    6.3.5
    When: 
    Wednesday, March 19 2014
    Time: 
    10:00
  • Using higher-order contracts to model session types

    Giovanni Bernardi

    FCUL

    Abstract: 

    Session types are used to describe and structure interactions between independent processes in distributed systems. Higher-order types are needed to properly structure delegation of responsibility between processes.

    In this talk we show that a sublanguage of higher-order web-service contracts provides a fully-abstract model of recursive higher-order session types. The model is set-theoretic, in that the meaning of a contract is the set of contracts with which it complies. The proof of full-abstraction depends on the novel notion of complement of a contract. We show that the new notion lets us type more well-formed programs than the commonly used type duality does, thereby improving existing type systems.

    Where: 
    6.3.38
    When: 
    Wednesday, March 12 2014
    Time: 
    10:00
  • Deadlock detection for general barrier synchronisation

    Tiago Cogumbreiro

    FCUL

    Abstract: 

    We present a formalisation of a general synchronisation mechanism that is adequate to detect barrier-based deadlocks, and develop a graph-based algorithm for detecting deadlocks that is sound and complete. Additionally, we establish an equivalence between task-centric and resource-centric detection algorithms, which increases the flexibility of designing deadlock detection tools. The expressiveness of the proposed barrier constructs are shown by surveying examples of common barrier idioms. The theory is materialised as a tool for detecting and recovering from deadlocked states in the X10 language.

    Where: 
    6.3.5
    When: 
    Thursday, October 31 2013
    Time: 
    9:30
  • Real-Time Integration: Improving Collaboration in Software Development

    Mário Guimarães

    FCUL

    Abstract: 

    Software systems are frequently complex and developed concurrently by several developers. This concurrent model of programming raises productivity, but it may cause conflicts between concurrent changes that must be resolved to avoid system failures.

    These conflicts must be detected early to prevent them from growing in number and complexity thus making their resolution harder. Recognizing this, solutions for early detection and resolution of conflicts have been proposed, however, among other limitations, they require developers to be proactive in detecting conflicts, which disrupts programming and wastes time if no real conflicts exist.

    Real-Time Integration is a new solution that automatically notifies developers when conflicts occur between concurrent changes. Conflicts are detected with high accuracy and precision, and presented to affected developers inside their IDEs, thus creating a concept of continuous merging by interleaving merging with programming. RTI includes novel features: few or no false positives, n-way structural merging, a conflict patterns language, and a metrics framework for comparison of conflict management tools. A popular IDE was extended to validate RTI via controlled studies, with graduate students and professionals, and showed that developers become aware of real conflicts earlier than in other solutions and with minimal overload.

    Where: 
    8.2.03 (pls note the excepcional room)
    When: 
    Wednesday, October 16 2013
    Time: 
    11:15
  • Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types

    Nobuko Yoshida

    Imperial College London

    Abstract: 

    Multiparty session types are a type system that can ensure the safety and liveness of distributed peers via the global specification of their interactions. To construct a global specification from a set of distributed uncontrolled behaviours, this talk explores the problem of fully characterising multiparty session types in terms of communicating automata. We equip global and local session types with labelled transition systems (LTSs) that faithfully represent asynchronous communications through unbounded buffered channels. Using the equivalence between the two LTSs, we identify a class of communicating automata that exactly correspond to the projected local types. We exhibit an algorithm to synthesise a global type from a collection of communicating automata. The key property of our findings is the notion of multiparty compatibility which non-trivially extends the duality condition for binary session types.

    Where: 
    6.3.5
    When: 
    Wednesday, July 24 2013
    Time: 
    11:00

Pages

Subscribe to Seminars