[PRL] POPL NOTES

Mitchell Wand wand at ccs.neu.edu
Tue Jan 18 18:21:19 EST 2005


Here are my notes on the talks I attended at POPL.  They are rather
long, but hopefully you'll be able to skim them.

--Mitch 

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

Tue Jan 11 21:01:12 2005

Attended the last session of PADL 

Role-Based Declarative Synchronization for Reconfigurable Systems
by Tananescu & Wojciechowski

Declarative synchronization like D, but done interpretively so that it
can be time-varying.  Use "roles" to identify threads, instead of
name-based pointcuts.  Karl might want to look at this.

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

Dengping Zhu & Hongwei Xi (BU)
Safe Programming with Pointers through Stateful Views

Mixes state assertions (a la Reynolds) with ordinary types to get some
safety properties for programs w/ pointers (including pointer
arithmetic).  Makes extensive use of singleton types and dependent
types to model arithmetic, etc., at the type level.  Worth looking
into if someone is interested in this topic.

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

Wang, Gupta, & Leuschel
Towards Provably Correct Code Generation via Horn Logical Continuation
Semantics

Something about compilation (to Prolog?) via partial evaluation.  The
claim is that their method is faster than others, but I didn't get
what was new here.  Perhaps Kenichi will find this paper readable.

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

The PADL PC presented a "most practical paper" award.  This went to 

A Provably Correct Compiler for Efficient Model Checking of Mobile
Processes by Yang, Dong, Ramakrishnan, and Smolka (SUNY Stony Brook).

This sounds worth looking into.  Something about model checking for
pi-calculus. 

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

At dinner, Frank Pfenning talked about female enrollments in CS at
CMU.  Their system is much like ours:  high school seniors choose
their school at application time, and CS there is a school, just like
it is at NU.

They had gotten up to 40% female enrollments.  Now it's down to 30%,
but that's still way better than we are doing.  Frank said that this
was the result of 3 things:

    1.  They do not consider previous programming experience when
        making admission decisions.  They just go with all the other
        regular criteria.

    2.  They have a bunch of support groups for women students (a
        "women in computer science" organization, etc.)

    3.  They bring in high school teachers and guidance counselors
        regularly (~ 400/yr) and tell them that they are making
        special efforts to recruit women into CS.

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

Wed Jan 12 08:50:22 2005

Rob Pike
[Google]

Interpreting the Data

Context:

8 Billion web pages x 10Kbytes/page = 80 Terabytes

100K machines.  If machines last 3 yrs, that's 100 machines that die
per day.

Google File System (GFS) labs.google.com/papers/gfs.html

Main part of talk: a DSL to get stats from their DB.

MapReduce: divides problem into pages, moves processing near GFS
machine with its data... sorts at 10GB/sec    papers/mapreduce.html
Visible remainder is very simple, usable by non-engineers.  

Looks at exactly one record at a time.  

Then uses associative commutative aggregators-- Some non-obvious
things are expressible as compositions of AC operators, eg top(100).

Can build tables out of these:

table top(1000) [country:string][hour:time] of string;

declares type of table of top 1000 items indexed by country and hour.

Sounds a lot like the Connection Machine.  He even said that he was
inspired by C*.

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

Compositional Compilation for Java

A Typed Intermediate Language for OOPs

>From the titles and descriptions, these looked like interesting the
papers.  But the presentations put me right to sleep.

Neil Glew said the second one of these was pretty good.

====

Appel has lecture notes on how to prove things in Twelf, in a way
that's very different from how the Twelf people do it.

====

Also, Appel says I should check out his Indexed Model of ADTs, with
McAlester (a few years old...)

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

Got a short tutorial on the C-machine from Bob Harper.

Hack: consider an A-receiving continuation as a *refutation* of A,
(rather than a proof of ~A).

Proofs M of A correspond to introduction rules,
Refutations K of A correspond to elimination rules
Machine state corresponds to a "contradiction" S ::= M#K.  

M ::= x | <M1, M2> | \x.M | (u x:- A)S              ;; introduction rules
K  ::= x | fst;K | snd;K | ([]M);K | (ubar x:A)S  ;; elimination rules

Typical rules:

<M1, M2> # fst;K  -> M1#K
(\x.M) # ([]N);K   --> M[N/x]
(u x:- A)S # K -> S[K/x]     (call/cc)
M # (ubar x: A. S) -> S[M/x]    

These M's are values!  Application is not primitive; it's replaced by
a CPS version, which can be either cbn or cbv.

The last two reductions form a critical pair, but it doesn't make any
difference which way you choose  (I'm not sure quite what Harper means
by that).

Problem is that the initial state M#K consists of a proof of A and a
refutation of A.  So there aren't any closed initial states.

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

Thu Jan 13 08:34:59 2005

Peter Selinger
Programming Languages for Quantum Computing

Fun presentation, alas I can't begin to summarize it.

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

Talked with Jens Palsberg.  He's got a system for checking when
inlining in Java is type-safe, even in presence of dynamic class
loading.

Issue 1:  Need flow analysis to see when inlining is possible, but
result may be too smart:  may not be able to inline "this".  So need
to have dumber FA that identifies fewer inlining sites.

Issue 2: Dynamic class loading means that some inlineable sites are no
longer safe to inlineable.  So inlining transformation looks like

(label l):x.m()  => if l in S then x.m() else ..inlined code...

S a dynamically-maintained set of invalidated types.

then dynamic class loading adds sites to S.

He knows about Hirzel's work on dynamic class loading (ECOOP 2003?)
and likes it. 

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

Stoyle, Michael hicks, Gavin Bierman, Peter Sewell, Iuian Neamtiu
Mutatis Mutandum: Safe & Predictable Dynamic Software Updating

Proteus: a C-like language w DSU.  (first order procedures, a heap).

e ::= .... let x = e1 in e2 | update

No functions in expression grammar; explicit update keyword means
updating is synchronous.

an update = function & named type replacements + func & named type
extensions.

Use only one-way (old-to-new) transformations.  Insert coercions where
necessary, and decline to update any program in which the old defn is
used concretely in the current continuation. (or something like that).

Static capability-based type system gives static prediction of what
types are updateable at each program point, so don't have to inspect
the continuation at run time.

Nice presentation, though slides were too small, as usual.

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

There was a discussion after lunch about the current practice of
disallowing submissions by members of the PC.  The consensus, by a 2-1
margin was that we should resume the old practice of allowing such
submissions.  The decision will be taken by the Steering Committee
later. 

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

John Field & Carlos Verela
Transactors: A programming model for globally consistent distributed
state

Motivating example:  internet-based home purchase-- a purchase in which all
the actors communicate via software instead of paper.  A nice example
for web services, harder than Orbitz.

What kind of PL abstractions can we find for handling this?

-- Core process calculus based on actor model.
-- State of each process is _explicit_
-- No guaranteed message delivery
-- Constructs for creating failure-resilient state _checkpoints_
-- Local failures cause rolback of local state to previous checkpoint]
-- Global state managed by piggybacking dependency information.

A transactor is like an actor, but it can:

-- stabilize : enter a mode where it does not change its state
-- checkpoint: create a consistent copy of current state.  Allowed only
   if t is stable.  After checkpoint,  t becomes volatile again.
-- rollback: reert to last checkpointed stae.

Semantics maintains dependence info about peer transactors.  My
impression is that this is an abstraction for hiding the (usual?)
stuff about nested rollback, etc.

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

Neubauer & Thiemann
>From Sequential Programs To Multi-Tier Applications by Program
Transformation

Interesting paper.  Title says it all.  (Again, slides were unreadable).

A questioner says: but the hard part is incorporating model of how
much it costs to move data from one tier to another, etc.  Doesn't
seem much hope of doing that in any automated way.


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

Benjamin Pierce et al.
Combinators for Bi-directional Tree Transformations

This is the work that Benjamin reported at NEPLS.  Very nifty.

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

Friday:

Pat Hanrahan, Stanford
How Should We Program Graphic Processors

Current GPUs faster than CPUs, and gap increasing, because they can
use VLSI resources more efficiently.

Programmable GPUs are stream processors (general-purpose!, not a
single-purpose pipeline).

Therefore a $50 high-performance, massively parallel computer is
shipping with every PC. (~ 60 GFlops, vs. 6 GFlops for a top of the
line Pentium).  This achieved by multiple pipelines (both parallel and
in series).  And GPU power is increasing faster than Moore's Law
(1.8-2.4, vs 1.5 for processors), but this may be an initialization
effect, since initial implementations were not so great.

So what's the right programming model for these things?

Answer: a Stream Model.  If you try to minimize state and processing
time/element, you are led to a stream model: do it one thing at time!
(echo of Rob Pike's talk here).  Each unit has a lot of processing but
a very small cache.

Model:  streams are collections of data records.  "Kernels" perform
computation on stream, can be chained together, etc.

Streams have predictable memory access patterns, can prefetch, etc.,
so don't need much/any cache.  This makes good match to hardware.

Arithmetic intensity = compute to bandwidth ratio.
eg.  bw: 1 vertex = 32 bytes, ops:  100-500 flops/vertex.

To increase intensity, want the primitives to be powerful, eg
dotproduct, not add & multiply.

With current hardware, need to do 8 flops/FPAccess (?) to keep
pipelines full. This number will likely increase.  This point is
optimal because then you spend half your money on computing and half
on communication/memory.

Jim Gray:  The Economics of Computing.  (He says everybody should read
this.  I've furled it, will grab url later).

Data parallel operations:  map, scan, reduce, send, sort, gather,
scatter, filter, generate.  He's implemented all of these on GPUs.

Approach 1:  map application to graphic-based PL model via libraries
(Open GL, etc.)

Aproach 2: map application to parallel computer.  So use an
intermediate PL like CSP etc.  {I didn't understand this step}

They've developed PE called "Brook": programmer need not know graphics
lib.  Versions for ATI & NVIDIA, Linux & Windows
sourceforge.net/projects/brook.

Because the GPUs are simple (no cache, etc).  compiling for them is
easier than for CPUs.  A simple compiler can get very close to a very
fancy one.

Get performance 1-7 faster on GPU vs. most optimized floatingpoint
benchmarks. 

Applications:  molecular dynamics (eg folding at home), fluid flow,
hidden markov models.

Summary: incredible opportunity for reinventing parallel compuing
software, programming environments and languages.

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

Matthew Parkinson, Gavin Bierman
Separation Logic and Abstraction

Want to do separation logic for ADTs, etc.  Need to scope predicate
definitions to support ADTs. 

Judgements now have predicate definition environments (\Lambda) on the
lhs of the turnstile

Lambda, Gamma |- {P}S{Q}     ;; I'll write P S Q

Separation logic.  Hoare Logic + a few extra things:

P*Q : means the heap can be split into 2 parts, one satisfies P the
other satisfies Q.

E -> E' the heap contains one location E and that location contains
E'.

Frame Rule:

P C Q
-----------
P*R C Q*R    if modifies(C) disjoint from fv(R)

Now want to have multiple memory managers...  

Can write specs for malloc and free.

Using uninterpreted predicates means we can't deduce things we
shouldn't know.

Rules for abstract weakening, abstract elimination allow you to move in
and out of abstraction boundaries.

Want to do classes and inheritance, each class has its own defn of the
abstract predicate.  So need abstract predicate _family_  Can
existentially quantify over subtypes.

Then need to rebuild rules, etc., but it's all straightforward.

Note technique of abstract predicates and AP families are orthogonal
from separation logic.

Future work:  compare w/ higher order separation logic [esop 05;
should check this out].

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

Richard Bornat (and a bunch of other people).
Permission Accounting in Separation Logic

Story:  malloc/new gives you a pointer to a new-ish buffer, you can do
what you like with the pointer.  free/dispose, given a pointer to a
buffer, takes the the buffer away.  You are left with a pointer (or
maybe several copies of it) which are are not allowed to use.

Slogan: typing isn't resourcing.  Typing is about static, value/state
independent properties of names.  Doesn't prevent you from taking
hd([]).

Resourcing adds the notions of quantity, value-dependence,
time-varying permission.

(If you think typing is everything that can be done satically, then
we're talking about the same thing).

About passing pointers in a heap resource that is shared among
concurrent processes.

Fractional permissions: Clever coding of permissions into reals in
[0,1]...  0 = nothing, 1 = r/w, anything else is read-only.

Some programs work better if you use some kind of counting
permissions.  Need both models.

Very nice presentation, should get the slides.

Possible application to G111 lectures??

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

Philippa Gardner et al
Context Logic and Tree Update

Separation Logic is about heap update.
Ambient Logic, etc is for reasoning abut trees.
Now want to merge these to reason about tree update: "context logic"

Want to do better than coding trees into heaps.

Tremendously lousy syntax, everything in subscripts.  Syntax is based
on ambient logic, but that's no excuse.

Unordered forests:

F ::= 0 | F*F (unordered composition)
     | a_n:p[F]    n the label of the node, p a possible pointer to
     another node.

Then introduce contexts (zippers) K,

Extend frame rule to

P C Q
--------------
K[P]  C  K[Q]          if modifies(C) disjoint from fv(K).

Get to quantify over tree contexts.

Then can produce nice rules for tree update in a context K.

Can specialize this to recapture ordinary heap contexts.
Also for terms, yields Hoare Logic for term rewriting.

Looks very neat.  Can it be used to quantify over continuations, etc?

Boy I wish Galen had had this when he did his factorization proofs.

I should write her and suggest our ESOP 02 paper as a possible
application.  Also BUBS.

Again, good slides, better than paper.

Side note:  I discovered that the symbol  -*  (adjunction implication) in
separation logic is pronounced "Magic Wand" (!)

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

Rinetzky Baueer Reps Sagiv Wilhelm
A Semantics for Procedure-Local Heaps and its Abstractions

How to paste abstract store back into main abstract store after a
procedure call that may alter memory.  This is the thing that Galen
spent a very long time worrying about.

Using "cutpoints" to capture sharing patterns in a uniform way.

Introduces "local heap operational semantics",  intermediate between
standard conc sem, and then the abstract semantics.

Storeless semantics:  represent object by the set of access paths that
point to it.  Heap is set of objects.  This is a concrete semantics--
ie it's precise.  Introduce "cutpoints", which are pointers from the
rest of the pgm into the relevant portion of the heap.  Then can paste
local heap back from procedure to caller, and everything works.

Now abstract this semantics like RWS.  The cutpoints are reified
nodes.

Claim is that this works BETTER on recursive procedures than on looping
programs.  

Very nice story on slides, but there's lot of details in the paper.

Q: How does this abstraction work for recursive procedures?  Ans:  "just
in the usual way", or "like external procedures".

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

Radu Rugina (& Brian Hackett)
Region-Based Shape Analysis with Tracked Locations

Idea 1:  combine heap analysis & pointer analysis.

Idea 2: reason abut one heap location at a time.  easier, more
efficient, inter-procedural.

Can use this analysis to detect memory errors.

Use 2 abstractions:

1.  use region abstraction like points-to analysis (looked like RWS,
    but I didn't see anything like indefinite nodes & pointers)  

2.  use shape abstraction: for each location keep track of 

    a) # of references to this location from each region, 
    b) access paths to this location and 
    c) list of access paths that definitely do NOT point to this
    location.  

Each of these can be computed independently, which makes life much easier.

Because analysis is per- (abstract)-location, interprocedural analysis
is simpler.

Good for acyclicity analysis

Limitation:  this abstraction doesn't capture doubly-linked lists.

Tim Reps says:  you need to add reachability abstractions to model
doubly-linked lists, shared lists, etc.

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

Gulwani & Necula
Precise Interprocedural Analysis using Random Interpretation

Random Interpretation = Random Testing + abstract interpretaton

Almost as simple as random testing but better soundnes guarantees.

Almost as sound as abstract interptation but more precise, efficient,
and simple.

Random interpretation executes program only once but by clever
abstract interpretation it captures all paths.

Generic algorithm:  choose random alues for input variables.  execute
assignments.  Use special "eval function" to evaluate expressions.
Execute both branches of conditionals and combine the states at join
points using "affine join function":

Given two pgm states s1 s2, then join(s1,s2)(y) = w*s1(y) +
(1-w)*s2(y), for some randomly chosen w (not necessarily in [0,1]).
Affine join preserves common linear relationships, eg a+b = 5, and
does not introduce false relationsips (with high probability).

Evaluation involves a syntactic transformation called "Poly".  This is
language dependent:

Linear arithmetic expressions (POPL 03): linear arithmetic, poly(e) =
e. 
 
Uninterpreted unary fcns (POPL 04)  e ::= y | F(e) ; poly(y) = y, poly(F(e))
= a*poly(e) + b .

Current paper shows how to extend this to interprocedural analysis.
Use random summary for IP analysis.  Analyze procedure by keeping
formal parameters symbolic, but using random choices for affine join.
This isn't quite sound, though:  Need to use different random
summaries for each procedure call.  This leads to exponential blowup
of number of summaries needed.  But can do this by random combination
of existing random summaries.

Big question:  how does this generalize to any more complicated things?

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

Sat Jan 15 09:11:44 2005 FOOL

Kim Bruce
Object-Oriented Languages, fixed points and systems of objects

Review: Classes are extensible generators of fixed points; objects are
fixpoints.

He introduces types ThisClass , @ThisClass (meaning -exactly- this
class). Can use these for binary methods (eg setNext in singly- and
doubly-linked lists -- if doubly-linked lists inherit from
singly-linked, then setNext needs to be covariant!).  Soundness of
typechecking in ECOOP 04.

Claim this works better than F-bounded polymorphism, which doesn't
play well with inheritance.

Expression problem:  see Sec 6 of Kim's WOOD 2003 paper.

Virtual types: when you specialize subject, then you need to
specialize observer and event classes.  Violates behavioral
subtyping. 

KB's solution:  "mutually recursive groups"; use @ThisTG (exactly this type
group) to get comon covariant specialization.

Dave MacQueen: the problem with "this" is that you don't know where
it's bound.  KB: yes, but that's what gives flexibility: it's variable
in classes, constant in objects.

KB: current languages overload classes as generators and as types.  He
prefers approach in which you use interfaces as types and classes as
generators only.

Phil Wadler: Good examples for type groups: (1) set of classes for
ASTs and then ASTs for the same grammar, but augmented with
attributes.  (2) lists of alternating types.  Then extend the list
with length information. (2) has the nice property that it fits on a
single page *without ellipses*!   {Good example for Honu!}

Note: KB used the PPT fadeout/fadein effect, which was very gentle
and pleasing.

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

Gavin Bierman & Alasdair Wren* 
First-class relationships in an object-oriented language

Interesting, though they made a number of design choices that seem
somewhat arbitrary.

Rebecca might be interested in this.

John Ridgeway:  might want to think about relationships as abstract
entities that can then be refined to use different implementation
techniques.

Phil Wadler: should check out work by Mark Wegman in which objects can
change roles/classes. (Also Fickle).

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

Sam TH* & Eric Allen
A Core Calculus of Metaclasses

Good presentation.

Q: cf Welty, What's in an Instance: Relation to ontology development?
Perhaps a class may have multiple relationships to other classes.

Q. Why isn't a static method of a class just an instance method of its
superclass?  A: We've thought about that.  Difficulty is constructors.

Andrew Black: what about upward and downward compatibility (well-known
in smalltalk?)?.  Sam gave an answer that AB seemed to find ok, though
I didn't understand it.

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

Dantas* & Walker
Harmless Advice

Harmless advice is advice that doesn't interfrere with main program
code.  Harmlessness is enforced by an information-flow type system.
Have proved non-interference property.

They did a small user survey: What do people use aspects for?  From
looking at mailing lists, it seems that people use aspects mostly for
tracing/logging/profiling and security checks/policy enforcement.
Conclusion: harmess advice that covers these categories will still be
useful.  So harmless advice should be able to output info from main
program and alter termination behavior.

So they define advice to be harmless if (for any pgm(?)) Pgm ->* Val
& Pgm+Aspect ->* Val'  , then val = val'  .   

Nice discussion of why the protection domains must be related the way
they are. 

Dantas graduates not in 2005, but maybe 5/2006.

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

Zenger & Odersky*
Independently Extensible Solutions to the Expression Problem

Essential constructs:  abstract types, mixin composition, and explicit
self types (for visitors).  These are also the core constructs of vObj
calculus).

He does it in Scala; Remy showed that you can do it in OCAML.

A trait is just a (possibly abstract) class without state.  Jens
Palsberg: Can we think of it as a typegroup a la KB?  Yes.

Need covariant adaptation.  Do this by defining an abstract type:

type exp <: Exp

Methods in subclasses use exp, not Exp.  They draw their value of exp
from the current instantiation.

But then need to instantiate the abstract type in order to instantiate
the framework, say

type exp = Exp; 

This binds exp to be the current binding of Exp.  This is "tying the
knot"-- you do this only at the end, when you are ready to close the
system.

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

Ernst*, Togerson, Hansen
Wild FJ

Wildcards are partially specified type argments to types.  Claim is
that these improve interaction among parametric & subtype polymorphism

OK, my brain is now officially fried.....

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

Panel on extreme typing:

Robbie Findler talked about contracts as a way of simulating a fancy
type system in a system with a simpler one.  Nice pictures, but was
too rushed to do more than introduce some analogies.


Jim Hook
Plunge into Extreme typing

Programmatica project at OGI: Building separation kernels (for
high-security systems) by monad composition.

Slogan: "type checking with a litle theorem proving".  Only kernel
must be scrutinized with general prOgram reasoning.  Kernel is 50
lines of Haskell code, out of several KLOC, if I understood this correctly.

Customer is a few US Govt agencies; current practice is to use a LOT
of theorem proving.  So anything that moves effort from thm prover to
type checker is helpful.

Some of this reported at FSC 03.

Very nice explanation of "the M word": monads are about explaining
sequencing, plus whatever other operations are there.  Sequencing must
be associative.

Q: Do people still care about security kernels?  A:  Some people still
do, though there is more diversity of opinion than there once was.

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

Wolfram Shulte, MSR.
Object Invariants Revisited:  an Example of Extreme Typing?

Project: Spec#, a rigorous C#.  Goal: enrich C# so that programmers
can document their assumptions.

What they did:

1. Refine type system.  Most common error is null pointers, so Spec#
adds non-null types, ala Cyclone or CCured.

2. Add contracts.  Enforce by mix of dynamic and static checking. Don't
worry about completeness or decidability.

Develop good defaults, eg: requires this.inv; modifies this.*; etc.

Issue: when do object invariants hold?  At the start of every public
method?  But this breaks in the face of callbacks.

public void Add(T sum)
   requires this.inv;
  {..
    expose(this){  //invalidate this env
     
     }

..}

Each object has a special boolean field inv, pgm invariant is o.inv =>
Inv(o), then get proof obligations....

More stuff about history and ownership to keep track of what can be
mentioned in an invariant.  Add extra owner field to keep track of who
owns what.  Add thread ownership to avoid data races.

So get very sophisticated system for generating verification conditions.

Looks neat!

(More stuff for G111/711 Invariants lecture?)

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

Jan Vitek
Stealth Typing

How do you convince people to use your type system?

Rules of the game: 0.  Pick a real language with a user base. 1. Don't
change syntax. 2. Can reinterpret existing constructs (they won't
notice!) 3. Pick a niche market. 4. Validate: demonstrate that this
buys you something.

Their example:  real-time specification for Java.  Memory model mixes regions
and garbage collection in a way that can blow up at run-time:  illegal
assignment, cyclic scope structure.

Approach: use scoped types, a variant of ownership types. Can get
static guarantee of no dynamic cycle/assignment errs.  This was
formalized in FJ and reported at RTSS04(!). (cf the competition,
Boyapati et al PLDI03.) 

[Who here was talking to me about RTJ?]

How to sell this extension to what is already an extension of Java?
Strategy:  encode the new stuff as a programming discipline (pattern?). 

Then validate empirically: refactor existing code base.  They took
Zen, a Java ORB, 100Kloc, used in a Boeing UAV, written in RTSJ at UCI
with a complex scope structure.

Done successfully.  They eliminated ~30 classes, with little code
duplication.  The software structure became (at least arguably) easier
to understand.  Several bugs were discovered.

This took ~2.5 man-months, starting with a grad student who didn't
know anything about ORBs, mostly in understanding existing code.  Then
using good refactoring tools like Eclipse was relatively easy.

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

Phil asked all presenters, including to panelists, to send him links
so that all the presentations will be available on FOOL web site.









More information about the PRL mailing list