Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

### viernes 19 de abril de 2013

11:00am Meeting room 302 (Mountain View), level 3

**Michael Emmi***, Post-doctoral Researcher**, LIAFA, Université Paris Diderot*

### Concurrent Software Modeling and Analysis: Recursively Parallel Programs

#### Abstract:

The widespread rigorous construction of concurrent software (e.g., reactive
event-driven code, high-performance parallel code, and geographically
distributed code) hinges on the development of effective programming
abstractions, the sound construction of the systems ensuring such abstractions,
and automated program analyses. My research investigates the specification of
such abstractions (e.g., atomicity specifications such as serializability and
linearizability), the formal modeling of computing platforms, including the
exploitation of such programming abstractions, and the pertinent program
analysis problems (e.g., whether a given implementation meets its specification
on a given platform). Besides studying the decidability and complexity of such
analysis problems, we develop problem approximations which yield more-tractable
algorithms for those highly intractable problems.

In one recent work, we have studied the so-called “explicitly-parallel”
programming languages developed for high-performance parallel computing. We
have proposed a general formal model of isolated recursive parallel
computations, and identified several fragments to match the features present in
real-world programming languages such as Cilk and X10. By associating
fundamental formal models (vector addition systems with recursive transitions)
to each fragment, we provide a common platform for exposing the relative
difficulties of algorithmic reasoning. For each case we measure the complexity
of deciding state-reachability for finite-data recursive programs, and propose
algorithms for the decidable cases. The complexities which include PTIME, NP,
EXPSPACE, and 2EXPTIME contrast with undecidable state-reachability for
finite-data recursive multi-threaded programs, thus exploiting the additional
computational structure imposed by these programming languages.