[MLton-devel] PLDI '03 Trip Report

[Stephen Weeks]

Talks
----------------------------------------
Lal George of Network Speed Technologies gave a talk, "Taming the IXP
Network Processor", on his and Matthias Blume's work on the Nova
Compiler for the Intel IXP processor.  The processor is very
constrained, and they use on integer linear programming to help with
register allocation/assignment.  Lal currently has a one man company,
Network Speed Technologies, with which he is trying to commercialize,
building the compiler in SML and using MLRISC for the codegen.

Mark Stephenson of MIT gave a talk, "Meta Optimization: Improving Compiler
Heuristics with Machine Learning", which I did not see, but I talked
with him later and he recommended genetic programming for tackling the
phase ordering problem we have in the MLton optimizer.  He also gave a
pointer to Cooper's work on the subject ("Optimizing for Reduced Code
Space using Genetic Algorithms").

Cristoph von Praun of ETH Zurich gave a talk, "Static Conflict
Analysis for Multi-Threaded Object-Oriented Programs".  I talked with
him some about their Java compiler, which does whole program analysis,
including the analysis described in his talk.  They're not focused on
performance, only the analysis.  In talking to several people, it
seems that there is a lot of interest, both academically and
commercially, in analyzing multithreaded Java programs for errors.

"Bug Isolation via Remote Program Sampling" was a cute talk.  The idea
was to instrument C programs to keep track of the relationships
between variables and the sign of the return values of functions.  The
random sampling can keep the overhead to a minimum.  Then, they can
analyze the data resulting from lots of program runs and find
correlations with program crashes.  Their technique helped to find a
bug in GNU bc undiscovered for over 10 years.

Mooly Sagiv of Tel-Aviv University gave a talk "CSSV, Towards a
Realistic Tool for Statically Detecting All Buffer Overflows in C".
The technique involves manually annotating procedures with pre and
post conditions which are verified by the tool and used for modular
checking.  They used it to verify a small part (400 lines) of the
Airbus code.  In the talk, he mentioned that their tool worked on some
code where a "commercial tool failed due to running out of memory" or
something like that.  I was curious if the commercial tool was
PolySpace's.  I talked to Mooly later and asked if there were any
plans afoot to commercialize this work and he said no.  I also asked
how the analysis compared to that of PolySpace, and he declined to
say.

Hai Fang of Yale gave a talk, "A Provably Sound TAL for Back-end
Optimization", joint work with Andrew Appel and others.  This work is
in the proof carrying code line, and continues their efforts to use a
small Trusted Computing Base.  They compile core SML to a low-level
IL, LTAL, and to SPARC machine code that is then checked by their LF
type checker written in C.  They modified SML/NJ, and in particular
MLRISC, to keep the necessary type information.  LTAL is very
expressive, and in particular can express data representations.  It
solves some of the holes that we have with the RSSA and MACHINE type
systems, most notably type checking case statements on datatypes even
with the low level tag selection and inspection code.  It would be
nice to adapt their ideas to our (simpler) ILs.

The best paper award went to "Automatically Proving the Correctness of
Compiler Optimizations", on which Sorin Lerner gave the talk.  They
have a special very simple language capable of expressing some
dataflow optimizations, which their tool can verify the correctness
of.  It's real in that they have implemented the tool and tested the
optimizations in their compiler.  But to my eyes it's a long ways from
helping us in the kinds of analyses we do in MLton.

"CCured in the Real World" covered their technique for keeping
metadata about C data structures so they can do safety checking at
runtime.  It's pretty neat, and even works with linked libraries
(although those of course remain unchecked). 

Other
----------------------------------------

I met Thomas Ball, of Microsoft Research.  They are using OCaml for
building programming tools.  He expressed some interest in an OCaml
front end for MLton, as they would like better performance.  I met
with a couple of other people from Microsoft Research, and all
expressed that there is a big push to improve their development tools
and hire people to work in that area.

I talked with Matthias Blume, who is now at Toyota Technology
Institute.  He is still working on CM, but not doing much on other
parts of SML/NJ.  I asked if anyone was, and he said that he was
probably working on it more than anyone.  The Yale group has forked of
FLINT and isn't feeding back much.  And there's nobody left at
Princeton.  Andrew Appel mentioned that he is no longer working on
SML/NJ -- he is just using it for the PCC/TCB/LTAL stuff.  So, SML/NJ
is no longer undergoing intensive development.

I talked with Greg Morisset, of Cornell University.  He mentioned that
he was thinking about automated testing tools to help avoid
re-introducing errors in the Cyclone compiler.  We also talked some
about an eager version of Haskell.  He mentioned that after his year
on sabbatical, he has come to appreciate the purity of Haskell, but
not the laziness.  Apparently, at POPL this year, even Simon Peyton
Jones said something to the effect that the laziness wasn't all that
essential. Anyways, I mention the idea of using MLton to develop an
eager Haskell and Greg sounded receptive.

I talked briefly with George Necula about CCured, which is implemented
in OCaml.  He mentioned that it has taken a long time to get the
parser right.  I also asked about the status of Cedilla Systems, his
startup with Peter Lee to do proof-carrying code for Java.  He said it
was in hibernation mode for now.

I talked with Norman Ramsey about a debugger for MLton.  He mentioned
that Sukyoung Ryu, a postdoc, is looking into MLton re debuggers, and
described some of the debugging infrastructure they are developing.
Norman also mentioned that C-- activity is picking up again.

I met Mark Tuttle, who is at HP Research Cambridge, and is using
MLton/SML for bounded model checking, which is model checking where
you don't have to check that the temporal logic property holds for all
the states, just for all the states reachable in some bounded number
of steps.  He has a 5K like SML program that translates a hardware
spec to a satisfiability problem, which he then uses some other tool
to solve.  After his initial port from SML/NJ to MLton, it ran 2X
faster.  Since then he has been playing with MLton's profiling tools.
He described an allocation performance bug that he found with the
allocation profiler, and as y'all saw in a recent email he is using
the time profiler too.  He said that the port took one or two days and
all in all seems happy with MLton.

I met Kwang Yi, who was presenting a paper at SAS, so I did not see
the talk.  He described a memory re-use analysis that they have in
their NML compiler (NML is a variant of SML).  It runs at about 1000
lines/sec, which isn't too bad, but a bit slow for MLton.  Who knows
how much it could be sped up though.

I heard from a couple of people about Sandburst (www.sandburst.com),
which is developing the Bluespec (www.bluespec.org) hardware
description language, which is based on Haskell and compiled to
Verilog.  People working at Sandburst include Arvind and Lennart
Augustsson, who gave a talk on Bluespec at ICFP 01.

Suresh and I talked about where the research areas are in MLton, and
what might make sense to write for POPL.  We thought some about
RSSA/MACHINE, but decided the focus was a little much engineering and
not enough new theory for POPL.  So, we decided the best place to
spend time is the opus.  I plan to spend a good chunk of time over the
next month or so on this.  Of course we'll all continue the discussion
in August.



-------------------------------------------------------
This SF.Net email is sponsored by: INetU
Attention Web Developers & Consultants: Become An INetU Hosting Partner.
Refer Dedicated Servers. We Manage Them. You Get 10% Monthly Commission!
INetU Dedicated Managed Hosting http://www.inetu.net/partner/index.php
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel