Wednesday, July 15, 2009


Viktor Kuncak gave the invited talk, the theme of which is his effort to get "verified abstractions on developers' desks". This boiled down to verifying library code, the hard part of which is accounting for the different state in the library vs. the application. He talked about his tool Jahob, which apparently does the business.

I chaired the first technical session of the day at IWACO, and it was the first session I've chaired at a workshop/conference, so I was a bit nervous. But all the talks were good and it went OK.

The first talk was by Nels Beckman and was about using access permissions to reduce STM overhead. This was a great little talk and had a great presentation of the various kinds of access and how they relate. The relation to STM was straightforward, but looked useful and they had empirical evidence to back it up - although 9% seems not too much of an improvement. It was also interesting that their optimisations incurred more overhead in some cases.

Eric Kerfoot presented the next talk, which used a very simple ownership scheme to avoid deadlock. Although the ownership aspects of this work were not that interesting (and probably not flexible enough for real life), it is good to see an application of ownership. The only problem being that the work seemed to be able to introduce more deadlocks if the wait clauses never become true.

William Retert presented the last talk of the session (and my favourite paper from the workshop) which compared everything even vaguely IWACO related using fractional permissions. This is a nice thing to do and something I'm very interested in seeing. I like being able to see exactly how these different mechanisms relate to each other. Unfortunately, other than encoding them all with fractional permissions, there wasn't much effort to then explain how these permissions relate at an intuitive level. I would have liked to see how their owners-as-effectors property relates to owners-as-modifiers, it is not quite a generalisation. I think it would also be interesting to extend the permissions beyond reading/writing to referencing so that owners-as-dominators could be expressed.

After lunch, Sophia presented work on flexible object invariants. The big point is that object invariants should be first class, and not just treated as syntactic sugar for pre- and post-conditions. An interesting example of invariants that can't be enforced in a tree-like structure are PIPs - Priority Inheritance Protocols, which involve cyclic structures.

I gave my first talk on wildcards in OGJ which went pretty well, and people seemed to 'get', although there was a bit of an atmosphere of "this is interesting, but so what?".

After the coffee break Paley spoke about combining ownership with relationships, in particular tackling the question of how relationships may be mutated with respect to their ownership properties. Finally I gave my second talk on comparing Universes and Ownership Types. Unfortunately, by this time I was mentally and physically exhausted and I was barely coherent for most of the talk and didn't handle the questions too well, which is a shame because the questions were really on point and I could have given more enlightening answers.

No comments: