[Pl-reading-group] PL seminars on Wednesdays (fwd)

Richard West 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.
> liulk
> 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
> http://cs3.bu.edu/mailman/listinfo/pl-reading-group


More information about the Pl-reading-group mailing list