Seminars

  • Runtime Programming

    Eduardo Marques

    FCUL

    Abstract: 

    We consider a methodology for flexible software design, runtime programming, defined by recurrent, incremental software modifications to a program at runtime, called runtime patches.

    The principles we consider for runtime programming are model preservation and scalability. Model preservation means that a runtime patch preserves the programming model in place for programs --- in terms of syntax, semantics, and correctness properties --- as opposed to an ``ad-hoc'', disruptive operation, or one that requires an extra level of abstraction. Scalability means that, for practicality and performance, the effort in program compilation required by a runtime patch should ideally scale in proportion to the change induced by it.

    We formulate runtime programming over an abstract model for component-based concurrent programs, defined by a modular relation between the syntax and semantics of programs, plus built-in notions of initialization and quiescence. The notion of a runtime patch is defined over these assumptions, as a model-preserving transition between two programs and respective states. Additionally, we propose an incremental compilation framework for scalability in patch compilation.

    The formulation is put in perspective through a case-study instantiation over a language for distributed hard real-time systems, the Hierarchical Timing Language (HTL).

    Where: 
    6.3.38
    When: 
    Wednesday, March 7 2012
    Time: 
    13:30
  • Proof Nets in Process Algebraic Form

    FCUL

    Abstract: 

    Process algebras suffer from the lack of logical foundations, in sharp contrast with λ-calculus which enjoys the Curry-Howard correspondence relating typed terms and Natural Deduction proofs. In this talk we present a Propositions-as-Types paradigm for concurrency: δ-calculus is a computational interpretation of Linear Logic, in the form of a typed process algebra whose structures correspond to Proof Nets -- the «Natural Deduction of Linear Logic» -- and where typing derivations correspond to linear sequent proofs. Term reduction shares the properties of cut elimination in the logic, and immediately we can obtain a number of inherited qualities, among which are termination, deadlock-freedom, and determinism.

    With respect to the notion of Programs-as-Proofs correspondence, we prove that for every Linear Sequent Proof there is a δ term typed with a (practically) identical sequent derivation, and the other direction, that for every well-typed term there exists a sequent proof. We will also show a sound and type-preserving translation to a linear λ-calculus, and finally a method that we conjecture to be sufficient in order to demonstrate that the language has the Church-Rosser (i.e., confluence) property.

    Where: 
    6.3.5
    When: 
    Wednesday, February 29 2012
    Time: 
    14:00
  • 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
  • Structured Communications: Global vs. Local and Imperative vs. Declarative visions

    Hugo Andres Lopez

    IT University of Copenhagen

    Abstract: 

    Our studies focus on two dichotomies when describing communications: the global/local points of view of a communication, and their imperative/declarative specification. In a global view a structured communication describes a process as a protocol for interactions, as e.g. a WS-CDL choreography or a UML sequence diagram. In a local view the system is described as a set of processes, e.g. specified as a pi -calculus or WS-BPEL process, implementing each participant in the process. While the global view is what is usually provided as specification, the local view is a necessary step towards a distributed implementation. The second dichotomy relates processes are specified: If processes are defined imperatively, the control flow is defined explicitly, e.g. as a sequence or flow graph of interactions/commands. In a declarative approach processes are described as a collection of conditions they should fulfill in order to be considered correct. Our thesis is that we can provide a theoretical framework based on typed concurrent process calculi for the specification, analysis and verification of structured communications which bridges the gap between the global and local views and combines the imperative and declarative specification approaches, and can be employed to increase the trustworthiness in the developed systems. This article describes our main motivations, results and future research directions. [Joint work with Marco Carbone, Davide Grohmann and Thomas Hildebrandt]

    Where: 
    6.3.5
    When: 
    Saturday, July 17 2010
    Time: 
    11:00
  • Plaid: a Resource-Based Language

    Jonathan Aldrich

    CMU

    Abstract: 

    As programming moves beyond algorithms and towards component composition and interaction with the world, managing software resources becomes increasingly difficult. Resources are objects whose use is constrained in some way. Example constraints include initializing resources before use, cleaning up resources when they are no longer needed, or following protocols such as checking for permission before performing an action on a resource.
    This talk describes how the Plaid programming language is designed to facilitate programming with resources. Rather than being an instance of a fixed class, every object in Plaid is in a state that is changeable. Like a class, each state has its own interface, representation, and behavior, allowing the source code to naturally model the conceptual evolution of objects.
    In order to help the programmer reason about resources, Plaid's permission-based type system tracks the state of objects and their aliases. Types are optional, and cast-like permission assertions enable the dynamic recovery of aliasing knowledge. Aliasing information in the type system allows Plaid programs to execute concurrently whenever operations are provably noninterfering. Together, these features support cleaner modeling of resource constraints, effective support in checking them, and efficient parallel execution on emerging multicore processors.

    Where: 
    6.3.5
    When: 
    Friday, May 21 2010
    Time: 
    11:00
  • Towards automated certification of cryptographic proofs

    Gilles Barthe

    IMDEA Software

    Abstract: 

    The game-based technique is a general method to prove the security of cryptographic schemes and protocols. Its code-based variant allows to view cast the correctness of a cryptographic scheme as a non-standard (probabilistic) program verification task, and relies on semantically well-established methods---relational Hoare logics, bisimulations, determinization. We will review earlier work on the
    formal verification of standard schemes in the Coq proof assistant, and present recent work on using
    automated methods based on SMT solvers.

    Where: 
    6.3.5
    When: 
    Friday, May 21 2010
    Time: 
    11:00

Pages

Subscribe to Seminars