Galois Tech Talk (2 of 3 next week!): Model-based Code Generation and Debugging of Concurrent Programs

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual time for this talk, it is on Wednesday, 11 January 2012

title: Model-based Code Generation and Debugging of Concurrent Programs

speaker: Borzoo Bonakdarpour

time: Wednesday, 11 January 2012, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Design and implementation of distributed systems often involve many subtleties due to their complex structure, non-determinism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We propose a method for generating distributed implementations from high-level component-based models that only employ simple synchronization primitives. The method is a sequence of three transformations preserving observational equivalence: (1) A transformation from a global state to a partial state model, (2) a transformation which replaces multi-party strong synchronization primitives in atomic components by point-to-point send/receive primitives based on asynchronous message passing, and (3) a final transformation to concrete distributed implementation based on platform and architecture. We study the properties of different transformations, in particular, performance criteria such as degree of parallelism and overhead for coordination.

The second part of the talk will focus on an automated technique for optimal instrumentation of multi-threaded programs for debugging and testing of concurrent data structures. We define a notion of observability that enables debuggers to trace back and locate errors through data-flow instrumentation. Observability in a concurrent program enables a debugger to extract the value of a set of desired variables through instrumenting another (possibly smaller) set of variables. We formulate an optimization problem that aims at minimizing the size of the latter set. Our experimental results on popular concurrent data structures (e.g., linked lists and red-black trees) show significant performance improvement in optimally-instrumented programs using our method as compared to ad-hoc over-instrumented programs.

bio: Borzoo Bonakdarpour is currently a research assistant professor at the School of Computer Science at University of Waterloo, Canada. He was a post-doctoral researcher at the Verimag Laboratory, France, working on the BIP project led by the 2007 Turing Award recipient, Joseph Sifakis. The aim of the project is to develop theory, methods, and tools for building real-time and distributed systems consisting of heterogeneous components. His other research interests include runtime verification, compositional verification of embedded systems, model synthesis and, in particular, automated model repair. He is the main developer of the tool SYCRAFT which is capable of synthesizing fault-tolerant distributed programs of the size 10^80 reachable states and beyond. Borzoo Bonakdarpour obtained his Ph.D. from the Department of Computer Science and Engineering at Michigan State University in 2009. His Ph.D. dissertation, "Automated Revision of Distributed and Real-Time Programs", studies a wide range of model repair problems in closed an open systems and was nominated for the 2010 ACM Doctoral Dissertation Award.

Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Formalizing Haskell 98 in the K Semantic Framework

speaker: David Lazar

time: Tuesday, 10 January 2012, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Formal semantics is notoriously hard. The K semantic framework is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework are modularity, expressivity, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of non-determinism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for correctness. These features made it possible to develop a complete formal semantics of the C language in K.

The first half of the talk will be an overview of the K semantic framework. We'll discuss the merits of the framework using the K definition of a complex toy language as a guiding example. The second half of the talk will focus on a work-in-progress formalization of Haskell 98 in K. We'll look at the challenges of formalizing Haskell and the applications of this work.

bio: David Lazar is an undergraduate studying computer science at the University of Illinois at Urbana-Champaign. He is one of several developers of the K framework. This summer, he worked on formalizing Haskell in K as a Google Summer of Code student.

Tech talk video: Candid Experiences from a Hardware Startup

We are pleased to announced the availability of a new tech talk video, Eric Migicovsky talking about his experiences with a hardware startup. More details about the talk are available at the talk announcement page. For more Galois tech talk videos, please visit our Vimeo channel.

Rapid, Consistent Web Development is Coming with HTML5

HTML5 is coming, and it’s not just the next version of HTML.

HTML began as a lightweight mark-up language for linking documents on the web, with some rendering hints. As new versions have come along, support has been added for new kinds of content (images, video, interactive content). More recently, interest has grown in understanding documents and web applications on a deeper level. The most prominent example of this is the semantic web, which seeks to move from a “web of documents” to a “web of information”.

All previous versions of HTML make this an extremely challenging task, akin to trying to understand a philosophical text presented in terms of its typography.

HTML5 will change that. The designers of HTML5 have taken great care to separate semantic content (the information a document is intended to convey or represent) from the process of rendering (how a document should appear in a browser). Through this “separation of concerns”, HTML5 is equipped to revolutionize how we think of the web, how we work with it, and how we create new content. Our interest is in the potential for HTML5 to change how we specify, design, build, and analyze user interfaces – wherever they may appear: on the web, mobile devices, or desktop.

With consistent user experience as our guiding motivation, we survey the state of the art and practice of tool support for semantic reasoning about HTML5.

Click to read more ...

Tech Talk: Frenetic: A Network Programming Language

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual time for this talk, it is on Thursday, 15 December 2011.

title: Frenetic: A Network Programming Language

speaker: Nate Foster

time: Thursday, 15 December 2011, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

The languages used to program networks today lack modern features. Programming them is a complicated task, and outages and infiltrations are frequent. We believe it is time to develop network programming languages with the following essential features:

• High-level abstractions that give programmers direct control over the network, allowing them to specify what they want the network to do without worrying about how to implement it.
• Compositional constructs that facilitate modular reasoning about programs.
• Portability, allowing programs written for one platform to be used with different devices.
• Rigorous semantic foundations that precisely document the meaning of the language and provide a basis for building formal verification tools.

. The Frenetic language addresses these challenges in the context of OpenFlow networks. It combines a streaming declarative query sub-language and a functional reactive sub-language that, together, provide many of the features listed above. Our implementation handles many low-level packet-processing details and keeps traffic in the "fast path" whenever possible.

bio: Nate Foster is an Assistant Professor of Computer Science at Cornell University. The goal of his research is developing high-level programming abstractions and tools for building reliable software systems. Specific topics of interest include language design and implementation, data management, networking, and security. He is the recipient of a PhD in Computer Science from the University of Pennsylvania, an MPhil in History and Philosophy of Science from Cambridge University, and a BA in Computer Science from Williams College. His work on bidirectional programming languages was awarded the Morris and Dorothy Rubinoff award for outstanding dissertation from Penn in 2009.