Seminars

  • Dynamic Deadlock Avoidance in Low-level Languages: Using Statically Inferred Effects

    Kostis Sagonas

    Uppsala University, Sweden and National Technical University of Athens, Greece

    Abstract: 

    Deadlocks are annoying and commonly occurring hazards associated with the concurrent execution of programs using locks. We have developed a polymorphic type and effect system that can be used to dynamically avoid deadlocks, guided by information about the order of lock and unlock operations which is computed statically. In contrast to most other type-based approaches to deadlock freedom, our system does not insist that programs adhere to a strict lock acquisition order or use locking primitives in a block-structured way. Lifting these restrictions is primarily motivated by our desire to target low-level languages, such as C with pthreads, but it also allows our system to be directly applicable in optimizing compilers for high-level languages, such as Java. To show the effectiveness of our approach, we have also developed a tool that uses static analysis to instrument concurrent programs written in C/pthreads and then links these programs with a run-time system that avoids possible deadlocks. Our benchmark results are very promising: they show that it is not only possible to avoid all deadlocks with a small run-time overhead, but also often achieve better throughput in highly concurrent programs by naturally reducing lock contention. More importantly, this is done without having to modify the original source program by altering the order of resource acquisition operations or by adding annotations.

    This is joint work with P. Gerakios, N. Papaspyrou and P. Vekris.

    Where: 
    6.3.5
    When: 
    Friday, October 21 2011
    Time: 
    13:30
  • Multiparty Session Types meet Communicating Automata

    Imperial College, University of London, UK

    Abstract: 

    Communicating finite state machines (CFSMs) abstract processes which communicate by asynchronous exchanges of messages via FIFO channels. Their major impact has been in characterising essential properties of communications such as freedom from deadlock and communication error, and buffer boundedness. CFSMs are known to be computationally hard: most of these properties are undecidable even in restricted cases. At the same time, multiparty session types are a recent typed framework whose main feature is its ability to efficiently enforce these properties for mobile processes and programming languages. This talk ties the links between the two frameworks to achieve a two-fold goal. On one hand, we present a generalised variant of multiparty session types that have a direct semantical correspondence to CFSMs. Our calculus can treat expressive forking, merging and joining protocols that are absent from existing session frameworks, and our typing system can ensure properties such as safety, boundedness and liveness on distributed processes by a polynomial time type checking. On the other hand, multiparty session types allow us to identify a new class of CFSMs that automatically enjoy the aforementioned properties, generalising Gouda et al's work GMY84 (for two machines) to an arbitrary number of machines. This is a joint work with Pierre-Malo Denielou.

    Where: 
    6.3.5
    When: 
    Wednesday, October 19 2011
    Time: 
    13:00
  • A process calculus-based logistics management

    Ichiro Satoh

    National Institute of Informatics, Japan

    Abstract: 

    This talk presents a process-calculus-based approach for managing logistics. We try to apply a process calculus to business management for logitics truck rather than concurrent/parallel computing. This is because logistics is just a parallel system consisting of multiple carriers, which exchange items between one another. We propose a language for specifying the routes of trucks and an order relation between the requirements of routes and the possible routes of trucks. The former is formulated as process calculus and the latter selects suitable trucks according to their routes. Our language and selection mechanism were implemented on a PaaS-based cloud computing infrastructure.

    Where: 
    6.3.5
    When: 
    Wednesday, October 12 2011
    Time: 
    13:00
  • Adaptable Processes

    Jorge A. Perez

    UNLisbon

    Abstract: 

    In this talk, I will propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime. This allows to express a wide range of evolvability patterns for processes. [Joint work with M. Bravetti, C. Di Giusto, G. Zavattaro - based on a paper to appear on FORTE'11]

    Where: 
    6.3.38
    When: 
    Thursday, September 15 2011
    Time: 
    11:00AM
  • Exogenous Combination of Logic Systems

    LaSIGE, DI, FC ULisbon

    Abstract: 

    Usually, the combination of two systems requires the translation of both systems to a common framework, where the combination is defined. In this talk we present a general technique to perform combination of logic systems. We call this method exogenous because it keeps unchanged the formulas and the models of the original logics. The results obtained on transference of (weakly) complete axiomatization and decidability are proven by providing sufficient conditions, on the morphisms and on the systems, to ensure the transference of such meta-properties. Finally, we motivate the applicability of our results on verification of probabilistic systems and on the study of probabilistic logics.

    Where: 
    6.3.5
    When: 
    Wednesday, July 6 2011
    Time: 
    11:00AM
Subscribe to Seminars