Seminars

  • 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
  • Interactive Interaction Constraints

    José Proença

    KU Leuven

    Abstract: 

    Interaction constraints are an expressive formalism for describing coordination patterns, such as those underlying the coordination language Reo, that can be efficiently implemented using constraint satisfaction technologies such as SAT and SMT solvers. Existing implementations of interaction constraints interact with external components only in a very simple way: interaction occurs only between rounds of constraint satisfaction. What is missing is any means for the constraint solver to interact with the external world during constraint satisfaction.

    This paper introduces interactive interaction constraints which enable interaction during constraint satisfaction, and in turn increase the expressiveness of coordination languages based on interaction constraints by allowing a larger class of operations to be considered to occur atomically. We describe how interactive interaction constraints are implemented and detail a number of strategies for guiding constraint solvers. The benefit of interactive interaction constraints is illustrated using two examples, a hotel booking system and a system of transactions with compensations. From a general perspective, our work describes how to open up and exploit constraint solvers as the basis of a coordination engine.

    Where: 
    6.3.5
    When: 
    Wednesday, July 17 2013
    Time: 
    14:00
  • Types for security and privacy of web data

    Jovanka Pantovic

    University of Novi Sad

    Abstract: 

    We present the XdPi calculus with role-based access control and a corresponding type system. This system is suitable for modeling distributed semi-structured web documents with dynamic role-based security administration. Our calculus is an extension of XdPi calculus of Gardner and Maffeis, where a network is a parallel composition of a process and a data tree. In our calculus, roles are assigned both to processes and trees. A process can read or modify data in a well-typed tree only if that role is assigned to the process. As each location has a specified policy, we show that the policy is respected during computation. A process can enable or disable a role if it is in accordance with the location policy. We discuss the policy maintenance of well-typed networks and present obtained security properties. Another important issue for publishing data on the web is privacy. The lack of privacy mechanisms can discourage people from making their data available and linked on web of data. Our current work focuses on development of a formal model which would ensure privacy protection of a single data in RDF format.

    Where: 
    6.3.5
    When: 
    Wednesday, July 10 2013
    Time: 
    14:00
  • Typing Progress in Communication-Centred Systems

    Hugo Torres Vieira

    FCUL & LaSIGE

    Abstract: 

    We present a type system for the analysis of progress in session-based communication centred systems. Our development is carried out in a minimal setting considering classic (binary) sessions, but building on and generalising previous work on progress analysis in the context of conversation types. Our contributions aim at underpinning forthcoming works on progress for session-typed systems, so as to support richer verification procedures based on a more foundational approach. Although this work does not target expressiveness, our approach already addresses challenging scenarios which are unaccounted for elsewhere in the literature, in particular systems that interleave communications on received session channels. [Joint work with Vasco Thudichum Vasconcelos]

    Where: 
    6.3.5
    When: 
    Wednesday, May 15 2013
    Time: 
    12:00
  • Coordinating phased activities while maintaining progress

    Tiago Cogumbreiro

    FCUL

    Abstract: 

    In order to develop reliable applications for parallel machines, programming languages and systems need to provide for exible parallel programming coordination techniques. Barriers, clocks and phasers constitute promising synchronisation mechanisms, but they exhibit intricate semantics and allow writing programs that can easily deadlock. We present an operational semantics and a type system for a fork/join programming model equipped with a exible variant of phasers. Our proposal allows for a precise control over the maximum number of synchronisation steps each task can be ahead of others. A type system ensures that programs do not deadlock, even when they use multiple phasers. [Joint work with Francisco Martins and Vasco Thudichum Vasconcelos]

    Where: 
    6.3.5
    When: 
    Wednesday, April 17 2013
    Time: 
    12:00
Subscribe to Seminars