[Nets-seminars] Fwd: Seminar Monday 4 Feb by PL Luminary, Mooly Sagiv

[Brad Karp]

I'd like to strongly encourage everyone in the Nets group (and anyone
else with an interest in solving hard computer systems research
problems) to attend this talk on Monday.

Mooly Sagiv is a leading light in the programming languages research
area. He will be giving a talk aimed at a general CS audience on Monday,
and the topic of his talk, how to synthesize correct data structures and
locking code for concurrent programs, is extremely timely given the
difficulty of programming today's multi-core machines.

Much of the best systems research involves drawing upon important
theoretical advances from areas like programming languages. Within the
Nets group, we tend to be too tunnel-visioned on the SIGCOMM, NSDI, and
SOSP proceedings (among others). This talk is an excellent chance to get
important exposure to new ideas in a highly relevant adjacent area. All
strongly encouraged to attend!

Thanks,
-Brad, bkarp at cs.ucl.ac.uk

-------- Original Message --------
Subject: Seminar 4 Feb by PL Luminary, Mooly Sagiv
Date: Thu, 31 Jan 2013 12:00:53 +0000
From: O'Hearn, Peter <p.ohearn at ucl.ac.uk>
To: research at cs.ucl.ac.uk <research at cs.ucl.ac.uk>

Mooly Sagiv form Tel Aviv University, one of the world's leading program
analysis researchers, is visiting the dept on 1 and 4 Feb. Mooly will
give a departmental seminar on Monday 4 Feb at 11am in MPEB 6.12 (sorry
for nonstandard time/place).

Attendance is encouraged. It would be great to have a reasonable turnout
for this distinguished visitor. His talk will be on data structure
synthesis, and is on the subject of a CACM Research Highlight article
(Peter Hawkins, Martin C. Rinard, Alex Aiken, Mooly Sagiv, Kathleen
Fisher: An introduction to data representation synthesis. Commun. ACM
55(12): 91-99 (2012))

Mooly will also give a more specialized technical talk on 1 Feb.

Peter


*****Talks by Mooly Sagiv****

DEPARTMENTAL SEMINAR, FOR GENERAL AUDIENCE

Time / date:	Monday 4th February 2013, 11am

Speaker:	Mooly Savig, Tel Aviv University

Location:	MPEB 6.12

Title:	Concurrent Data Representation Synthesis

Abstract:	We describe an approach for synthesizing data representations
for concurrent programs. Our compiler takes as input a program written
using concurrent relations and synthesizes a representation of the
relations as sets of cooperating data structures as well as the
placement and acquisition of locks to synchronize concurrent access to
those data structures. The resulting code is correct by construction:
individual relational operations are implemented correctly and the
aggregate set of operations is serializable and deadlock free. The
relational specification also permits a high-level optimizer to choose
the best performing of many possible legal data representations and
locking strategies, which we demonstrate with an experiment autotuning a
graph benchmark.

 	This is joint work with Alex Aiken and Peter Hawkins(Stanford),
Katleen Fisher(DARPA), and Martin Rinard(MIT)

 	This work is part of Peter Hawkins thesis theory.stanford.edu/~hawkinsp/

        Please also look into the  December CACM article

---------------------------



PPLV SEMINAR

Time: Fri 1 Feb, 4-5pm

Location: Executive Suite 103 & 104, Engineering Front Building, Malet
Place, UCL

Title: Effectively-Propositional Reasoning About Reachability

Abstract: This paper proposes a novel method of harnessing existing SAT
solvers to verify reachability properties of programs that manipulate
linked-list data structures. Such properties are essential for proving
program termination, correctness of data structure invariants, and other
safety properties. Our solution is complete, i.e., a SAT solver produces
a counterexample whenever a program does not satisfy its specification.
This result is surprising since even first-order theorem provers usually
cannot deal with reachability in a complete way, because doing so
requires reasoning about transitive closure.

Our result is based on the following ideas:

1.  Programmers must write assertions in a restricted logic without
quantifier alternation or function symbols.

2.  The correctness of many programs can be expressed in such restricted
logics, although we explain the tradeoffs.

3.  Recent results in descriptive complexity can be utilized to show
that every program that manipulates potentially cyclic, singly- and
doubly-linked lists and that is annotated with assertions written in
this restricted logic, can be verified with a SAT solver.

We implemented a tool atop Z3 and used it to show the correctness of
several linked list programs.