[Pl-seminar] Two possibly interesting talks today

[Mitchell Wand]

From: Csail Event Calendar <eventcalendar at csail.mit.edu>
To: seminars at csail.mit.edu
Date: Thu, 31 Mar 2011 00:01:02 -0400
Subject: TALK:Thursday 3-31-11 Verifying Low-Level Implementations of
High-Level Datatypes

Verifying Low-Level Implementations of High-Level Datatypes
Speaker: Clark Barrett
Speaker Affiliation: New York University
Host: Daniel Jackson
Host Affiliation: CSAIL

Date: 3-31-2011
Time: 3:00 PM - 4:00 PM
Location: 32-G882 (Hewlett Room)

For efficiency and portability, network packet processing code is typically
written in low-level languages and makes use of bit-level operations to
compactly represent data. Although packet data is highly structured,
low-level
implementation details make it difficult to verify that the behavior of the
code is consistent with high-level data invariants. We introduce a new
approach to the verification problem, using a high-level definition of
packet
types as part of a specification rather than an implementation. The types
are
not used to check the code directly; rather, the types introduce functions
and
predicates that can be used to assert the consistency of code with
programmer-defined data assertions. We describe an encoding of these types
and
functions using the theories of inductive datatypes, bit vectors, and arrays
in the CVC3 SMT solver. We present a case study in which the method is
applied
to open-source networking code and verified within the Cascade verification
platform.

Bio:

Clark Barrett is an associate professor at New York University. His research
interests include propositional satisfiability (SAT), satisfiability modulo
theories (SMT), automated deduction and applied logic, proof-producing
algorithms, formal and semi-formal verification of hardware and software,
and
combining verification systems. He was recently awarded the Haifa
Verification
Conference award (2010), along with Leonardo de Moura, Silvio Ranise, Aaron
Stump, and Cesare Tinelli, for his pivotal role in building and promoting
the
Satisfiability Modulo Theories (SMT) community.

Relevant URL(S):
For more information please contact: Eunsuk Kang, eskang at csail.mit.edu


=======================================

> *From: *Nicolas Pinto <pinto at mit.edu <mailto:pinto at mit.edu>>
> *Date: *March 30, 2011 11:29:42 PM EDT
> *To: *undisclosed-recipients:;
> *Subject: **TALK: cl.oquence: High-Level Language Abstractions for
> Low-Level Programming (Cyrus Omar from CMU, Thursday March 31st,
> 2011, 8:35 PM, Harvard Hall 104)*
>
> Title: cl.oquence: High-Level Language Abstractions for Low-Level
> Programming
> Speaker:  Cyrus Omar (CMU)
>
> Date: 3-31-2011
> Time: 8:35 PM
> Location: Harvard Hall 104 **Room change**
>
> Harvard CS264 2011 Guest Lecture Series
> "Massively Parallel Computing" Course (http://www.cs264.org)
> Host: Nicolas Pinto (Harvard, MIT)
>
> Abstract:
>
> When performance is important, developers turn to "low-level"
> languages like C, FORTRAN, CUDA and OpenCL. These languages handle
> issues related to register and stack allocation for their users, but
> do not otherwise attempt to manage memory allocation or control data
> movement. Developers continue to favor this design, despite the
> increased development burden, because small changes to an algorithm's
> data movement patterns can dramatically impact overall performance on
> modern hardware, including GPUs, but compilers for high-level
> languages are not yet able to reliably outperform motivated human
> experts. Indeed, the most prominent productivity-oriented languages in
> computational science -- MATLAB and Python -- come with significant
> performance overhead.
>
> In this talk, I will demonstrate that many of the
> productivity-enhancing features characteristic of high-level languages
> can be reconciled with a low-level programming model with no
> performance penalty, using techniques like type inference, structural
> polymorphism and compile-time metaprogramming. The resulting language,
> called cl.oquence, compiles directly into OpenCL source code. Because
> OpenCL is low-level, supports a variety of architectures and can be
> called from several languages, cl.oquence functions can be integrated
> into existing projects easily. For Python users, special bindings have
> been developed, based on pyopencl, that allow users to write
> cl.oquence functions inline and call them directly, without even the
> minimal syntactic overhead that a more generic binding would require.
>
> Although the language remains in beta, I have been using it to run
> large-scale neurobiological circuit simulations. An informal case
> study of this simulation framework will be presented. The language is
> free, open-source and well-documented. It will be available at
> http://cl.oquence.org/ shortly. Interested people can email me
> (cyrus at cmu.edu <mailto:cyrus at cmu.edu>).
>
>
> Speaker biography:
>
> Cyrus Omar is a graduate student in the Computer Science Department at
> Carnegie Mellon University. His research focuses on building better
> programming languages, compilers, development environments and data
> sharing infrastructure for computational science and high-performance
> computing, with a particular focus on computational neurobiology.
> http://www.cs.cmu.edu/~comar <http://www.cs.cmu.edu/%7Ecomar>
-------------- next part --------------
HTML attachment scrubbed and removed