[Pl-reading-group] PL seminars on Wednesdays (fwd)
richwest at cs.bu.edu
Thu Mar 19 09:05:56 EDT 2009
I thought this was a well-presented talk yesterday, with a pretty clear
explanation of the ATS specifics. Now that I've seen several talks from
the PL group on ways to address type semantics of system and library calls
(e.g., mmap and fork) I think I realize where the key issues are from a
safe programming perspective.
For example, with mmap(), a systems programmer is probably less interested
in getting the flag settings correct but more interested in making sure
a mapped file is not being modified uncontrollably via another channel.
Specifically, if one process mmaps a file and another process is using
read/write system calls on a file descriptor to the same file then the
contents of what is mmaped may be changed in an ad hoc manner.
So, what is the issue with safety of system calls and libraries?
I really think it comes down to the complex interaction of these calls
rather than any one individual call. Now, that may sound depressing since
we want to do more than tighten up the typing rules on an individual
function and, preferably, define ways to avoid unexpected side-effects
when we combine function calls.
Another classic example would be if we issued a malloc call within a
signal handler. Individually, sigaction() and malloc() might have
well-defined types but then how do we address the problem of re-entrancy
on heap data structures as manipulated by the malloc call itself if it is
invoked asynchronously? Similarly, what if we try to acquire a lock using
some mutex-acquisition call from within a signal handler, when that lock
is already held? It seems to me we need some control-flow analysis here.
On Tue, 17 Mar 2009, LiKai Liu wrote:
> Date: Tue, 17 Mar 2009 16:05:49 -0400 (EDT)
> From: LiKai Liu <liulk at cs.bu.edu>
> To: <pl-reading-group at cs.bu.edu>
> Subject: Re: [Pl-reading-group] PL seminars on Wednesdays (fwd)
> Just reminding everyone of the talk tomorrow.
> On Thu, 19 Feb 2009, LiKai Liu wrote:
> > Title: Expressing the type of mmap() system call in ATS
> > Abstract: The POSIX standard specifies a mmap() system call that allows
> > programs to request memory pages to be mapped into the current process
> > address space. The memory pages could be backed by system's swap file or
> > an arbitrary disk file, and the programmer specifies such intent by
> > passing integer bit flags. Integer bit flag is a common way in the C
> > language to pass a set of options to a function. A bit's zero and one
> > value indicates membership of the option represented by the bit. In the
> > case of mmap(), the prescence and absence of certain bit flags changes the
> > resource requirement: if you want to map a disk file, then you need to
> > give a valid file descriptor; otherwise you don't need a file descriptor.
> > In this talk, I will show how to express bit flags in ATS in a way that
> > will make the type checker aware of appropriate resource requirements
> > indicated by the flag.
> > Speaker: Likai Liu
> Pl-reading-group mailing list
> Pl-reading-group at cs3.bu.edu
More information about the Pl-reading-group