Seminars

  • Certifying Data in Multiparty Session Types

    Bernardo Toninho

    Imperial College London

    Abstract: 

    Multiparty session types are a typing discipline and methodology to
    ensure communication safety in protocols involving two or more
    concurrent participants.

    In this talk I will present the integration of value dependent types
    in a multiparty session typed framework (i.e. types that depend on the
    exchanged data values), enabling static assurances of not only
    communication safety but also of properties of the data itself.
    I will discuss the main tensions, challenges and trade-offs of
    adopting such a framework in the context of multiparty conversations,
    as well as a few simple extensions that increase the flexibility and
    expressiveness of the framework such as so-called “ghost variables” and
    provenance information tracking in a distributed setting.

    I will also elaborate on some potential avenues of future research based
    on this framework.

    Where: 
    6.3.5
    When: 
    Thursday, December 17 2015
    Time: 
    9:30
  • A Data Manipulation Language for Heterogeneous Environments.

    João Costa Seco

    FCT / Universidade Nova de Lisboa

    Abstract: 

    One key aspect of data-centric applications is the manipulation of persistent data repositories, which is moving fast from querying a centralized relational database to the ad-hoc combination of constellations of data sources. Query languages are being typefuly integrated in host, general purpose, languages in order to increase reasoning and optimizing capabilities of interpreters and compilers. However, not much is being done to integrate and orchestrate different and separate sources of data.

    We present a common data manipulation language, that abstracts the nature and localization of the data-sources. We define its semantics and a type directed compilation, query optimization, and query orchestration mechanism to be used in development tools for heterogeneous environments. We provide type safety and language integration. Our approach is also suitable for an interactive query construction environment by rich user interfaces that provide immediate feedback on data manipulation operations. This approach is currently the base for the data layer of a development platform for mobile and web applications.

    (joint work with Paulo Ferreira and Hugo Lourenço, OutSystems SA)

    Where: 
    6.3.38
    When: 
    Wednesday, December 2 2015
    Time: 
    16:00
  • Ownership and Reference Counting based Garbage Collection in the Actor World

    Juliana Franco

    Imperial College London

    Abstract: 

    We propose Pony-ORCA, a fully concurrent protocol for garbage collection in the actor paradigm. It allows actors to perform garbage collection concurrently with any number of other actors. It does not require any form of synchronization across actors except those introduced through the actor paradigm, i.e., message send and message receive.

    Pony-ORCA is based on ideas from ownership and deferred, distributed, weighted reference counting. It adapts the messaging system of actors to keep the reference count consistent.

    We introduce a formal model and describe the invariants on which it relies. We illustrate these invariants through an example and sketch how they are maintained. We show some benchmarks and argue that the protocol can be implemented efficiently.

    Joint work with Sylvan Clebsch, Sebastian Blessing and Sophia Drossopoulou.

    Where: 
    6.3.5
    When: 
    Thursday, July 2 2015
    Time: 
    11:30
  • Erlang multicore applications

    Wojciech Turek

    AGH University of Science and Technology, Krakow, Poland

    Abstract: 

    The development of multi-core architectures is incredibly fast and multicore CPUs can be found nowadays not only
    in supercomputers, but also in ordinary laptops or even phones. Efficient use of multicore architectures requires applying suitable languages and technologies, like Erlang.
    Its concurrency model, based on lightweight processes and asynchronous message-passing, seems very well suited for running massively
    concurrent code on many cores. Most of existing Erlang industrial applications are deployed on computers with up to 24 CPU cores, and
    there are hardly any reports on using Erlang on architectures exceeding 32 cores. We present our experiences with scaling a
    computationally-intensive applications in Erlang up to 64 cores, using as examples global optimization and urban traffic planning problems.

    Where: 
    6.3.5
    When: 
    Thursday, June 4 2015
    Time: 
    11:00
  • 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
Subscribe to Seminars