How is Aliasing Used in Systems Software/KennKnowles
From GradTurkey
zelbascercn Response to How is Aliasing Used in Systems Software
[edit] Prior Analyses
- Imprecision
- They mention the folklore that analyses tend to have a few well-analyzed portions with nice understandable structure, and then the blob. It is valuable just to shrink the blob, but this also hints at the fact that the blob should also have understandable structure; the structure exists in programmers' minds even if we don't know how to analyze it.
- Measurement
- This paper contains a lot of numbers and proportions of types of aliasing and false positives. The real scientific nature of the investigation sets it apart.
[edit] Annotations
The annotations seem quite reasonable, though one would have to look at the exact annotations needed. The rate of annotation is small, and as expected a few key annotations on data type definitions do wonders. It is interesting (and surprising to me) that a number of the annotations already existed in comments. Making comments into automatically checked specs is always good.
One must wonder whether, since these annotations fall into a few key classes of aliasing, there is a good linguistic model for the concepts that could result in some very fast, easy, and routine analysis (like types are now).
A limitation of the annotations may be a lack of "must" and "may" distinctions. I don't have a great intuition as to whether this matters, but for function summaries, sometimes a function really doesn't care if things are aliased. This doesn't seem to be a limiting aspect of the work, anyhow.
[edit] Misc Comments
- The most dangerous aliases sound like I/O aliases, which amount to communication channels. This suggests that an easy "channel" abstraction with atomic read/write operations would be a good replacement for a large number of aliasing errors.
- They very briefly mention a kind of polymorphism, but I think it probably deserves more treatment, since polymorphism (the ML kind, not the Java kind) in existing systems is arguably what has brought statically typed languages to such a high level of abstraction.
- While C is very popular, the culture surrounding Java and ML are quite different, and I would be curious how the taxonomy breaks down there. In ML, for example, one must only examing mutable reference, of course, and they are fairly rare. What does this even mean for Haskell? Nothing? Is there a high level pointer language out there (because C sure isn't)?
