The Theory and Calculus of Aliasing

I have done some work recently on the theory of aliasing, which I believe provides the key to the frame problem and more generally to proving O-O programs (although these applications remain to be better explained and explored further).

I was struck by the simplicity and generality of the laws uncovered in the process.

A blog entry at bertrandmeyer.com presents the basics. It includes a link to the draft paper, and also to a downloadable version of the implementation (currently a Windows executable, the source will be released later), which makes it possible to test all the examples of the paper.

-- Bertrand Meyer

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Very interesting. How does

Very interesting. How does this work relate to various alias analyses in compilers?

The Frame Problem?

Could you clarify what you're referring to as "the frame problem?" Is it the one that arose in AI research? To wit, The Frame Problem

Frame problem

By "frame problem" I (and I hope others, although there is always a risk of believing one's terminology is shared beyond a small community) mean the general question of specifying and proving what does not change in an operation. Contracts typically specify what changes and how it changes: in a bank withdrawal operation, the account's balance gets decreased by the specific amount. They seldom exhaustively state what does not change: the withdrawal operation should not replace the name of the account holder, the account number, the name of the bank. Full-fledged proofs must work with complete specifications that handle both kinds of properties.

This is indeed related to the AI notion of frames as defined by Minsky in the seventies, but with a specific software engineering meaning.

One nit

This is indeed related to the AI notion of frames as defined by Minsky in the seventies, but with a specific software engineering meaning.

Frame problem was described by McCarthy, and has had some famous attempts at solving it, most notably using circumscription that failed on the Yale shooting problem counter-example [1]. Frame problem is not really related to frame languages, as described by Minsky. In Society of Mind, Minsky opines that his sheer dumb luck in writing that paper was that he was vague just enough so that others would be inspired to flesh it out in tangential ways. He then notes that sometimes being too formal with new ideas can make them harder for others to embrace, and that it turned out his vague specification was a blessing in disguise. Paul G. Bassett also describes a different frame language in his book, Framing Software Reuse, which can best be thought of in today's terminology as an invasive software composition system (using Frame-Oriented Programming 'adapt' composers); it is also mostly unrelated to the frame problem.

Many ideas related to the frame problem have their roots in AI, but also in term rewriting. Rewriting logic solves the frame problem by phrasing the problem in terms of concurrent action and change. See this paper by two Maude weenies.

[1] For what it's worth, the solution to this problem in circumscription-based logic is known as the commonsense law of inertia: things are guaranteed to stay the same unless they are affected by an event.

McCarthy / Minsky

Thanks for correcting me regarding the anteriority of McCarthy's paper (http://www-formal.stanford.edu/jmc/mcchay69/node17.html#SECTION00043000000000000000). Minsky's 1974 paper (http://web.media.mit.edu/~minsky/papers/Frames/frames.html) was the one through which I first learned about the topic.

You're right

Sorry, Bertrand.

After re-reading Minsky's essay carefully (it's been awhile), he does cover the frame problem, but does not refer to it as such. Instead, he refers to the frame problem as a problem of defining "a 'minimal' common-sense system".

FORMALIZING THE REQUIRED KNOWLEDGE: Just constructing a knowledge base is a major intellectual research problem. Whether one's goal is logistic or not, we still know far too little about the contents and structure of common-sense knowledge. A "minimal" common-sense system must "know" something about cause-and-effect, time, purpose, locality, process, and types of knowledge. It also needs ways to acquire, represent, and use such knowledge. We need a serious epistemological research effort in this area. The essays of McCarthy {} and Sandewall {} are steps in that direction. I have no easy plan for this large enterprise; but the magnitude of the task will certainly depend strongly on the representations chosen, and I think that Logistic is already making trouble.

It's clear, upon re-reading it with the frame problem in mind, that Minsky is referring to the frame problem. The last time I read this essay, the McCarthy citation was {} as it is now, so I made no connection to it.

Typo?

Was the line following "The rule for creation is the same as for forget:" supposed to mention create? (Apologies for the insignificant comment)

Fixed

Thanks a lot! Sorry for the typo (copy-paste error), now corrected.

The evil of aliasing

The paper looks fascinating, though I have only looked at some of it.

I wonder if I am right in thinking that things like possible overlap
between storage buffers is a phenomenon like aliasing? I am thinking
of a memcpy procedure that has to decide in case of possible overlap
whether to copy by increasing or decreasing addresses. This in itself
is not so expensive -- the problem is what to say in case the copy
is interrupted. If their is overlap, one should probably say that
the content of *both* buffers is trashed, ie unpredictable. So the
specification is damaged, never mind the implementation being more
complicated.

Somewhere else that aliasing seems a central issue is in garbage
collection of linked structures, where lack of potential sharing
can be very nice indeed (co-evil). (Its been known for a long
time that garbage collectors can themselves perform certain kinds
of reduction.)

indeed

Other applications

The paper looks fascinating, though I have only looked at some of it.

Please read all... I think the most important parts come towards the end, but the buildup is necessary.

It would be interesting to look at applications to buffer overlap. As it is, however, the alias calculus assumes a typed framework, so I don't know how it transposes to a word of addresses and untyped pointers. But it's worth looking into.

Seems useful for proving authority limits

Hi Bertrand,

Your work on aliasing seems like it might be useful for proving limits on the propagation of permission and authority, as for example I examine informally in Robust Composition and Fred Spiessens' formalizes and mechanically proves in his Patterns of Safe Collaboration. The first problem Fred examines, the Caretaker, is all about ensuring graph disjointness after revocation, assuming disjointness before introduction.

Also see part 3 of Robust Composition, where I deal with plan interference by interleaving, even in sequential programs, and how to avoid them by postponement. The plan interference hazard with the sequential StatusHolder is due to the possibility of an access path from the listener back to the StatusHolder. Postponement (by eventual send) may be a bigger hammer than is needed if we imagine a convenient way to instead ensure the absence of this aliasing path.

Do you imagine an integrated notation which would let us express the needed constraints on aliasing within a program, so that the safety of Caretaker or the sequential StatusHolder would follow?

Thanks

Thanks for the references, I have started reading them. Applications to concurrency are indeed next on my agenda, although I was thinking more of issues like deadlock in SCOOP than of security, so I appreciate the hint.

applicability to real OO Software

It is very interesting to introduce the “alias relation”. With this relation a lot of reasoning can be done as you have demonstrated well in your draft paper “The theory and Calculus of Aliasing”.

I like the fact, that no new notation is necessary in the program text. This is an advantage over dynamic frame contracts.

You build the alias relation bottom up, starting from elementary statements (i.e. the effect of the statements on the alias relation) to more complex statements.

But this might be also one of the weak points to solve the framing problem for OO Software. As far as I have understood your theory, it does (in its current state) not go well with dynamic binding and modular reasoning. Consider a parent class which introduces some deferred features (i.e. features with contracts only). A client using these features does not see the implementation.

How can you calculate the effect of a call to a deferred routine on the alias relation? If you do dynamic typeset calculation you can calculate the union of all effects. But then you leave modular reasoning. If you want to stick to modular reasoning, you certainly have to introduce some notation for deferred features to specify the effect on the alias relation which is binding for the descendants (like Bernd Schoeller did for his frame contracts).

Aliasing Calculus vs. Implementation Hiding

I share this concern. My first questions were how this 'aliasing calculus' could possibly be relevant in the presence of implementation hiding (and its cousins, such as distributed programming). Given that implementation hiding is at the core of OOP, I don't see how it will be relevant for anything but local optimizations of certain patterns (e.g. the capability revocation and other 'interference' patterns mentioned by MarkM).

Linear typing is somewhat more promising, allowing aliasing concerns and exclusive rights transfers to be enforced to some degree. Locally, it is subject to type-checking or language-layer enforcement. The sort of exclusive transfer of rights supported by various 'smart contracts' protocols might even allow linear typing to work with a distributed protocol, though I can only imagine there would be a rather hefty performance and communications cost associated with achieving that (i.e. essentially requiring the right be renamed to finalize each transfer crossing trust or security domain boundaries).

In any case, I share your difficulty in seeing how this alias calculus would be useful to me. If it cannot be applied at the interface level, then it certainly isn't useful for analysis of 'large' software. It isn't even clear what sort of features (optimizations, data-flow analysis, etc.) might be achieved via its local application.

Perhaps someone with the big-picture view can explain where Aliasing Calculus might be useful?

Aliasing is not compositional

Since Mr. Brandl posted the same comment next to the original referred entry, I responded there. Let me mention, though, that his post provides excellent (informal) evidence of the difficulty of the issue. Looking at the original blog, we could deduce that he did not make any comment related to a comment by Jules Jacobs. Now if I add there (as I now did for the sake of the argument) that “comments #1 and #13 on the first external blog referring to this topic are related”, I introduce an aliasing of sorts between the two authors, which is only visible when we consider the two blogs together.

See the full response at the given URL.

Modularity?

Application to "large" software is the subject of the forthcoming companion paper. I disagree, however, with your point that "if it cannot be applied at the interface level, then it certainly isn't useful for analysis of 'large' software". First, this is wishful thinking: you want modular (compositional) techniques, which is certainly a goal to sympathize with, but what if the problem is essentially non-compositional? Second, in practice, if you are in charge of a mission-critical development and have to sign as statement that the software is correct, you will want to verify the full thing anyway, not rely blindly on someone else's guarantee that some routine or class is correct.

In my opinion modularity is highly desirable, but if it is not applicable to a particular problem we have to accept the pain and move on.

Software Is Composition

what if the problem is essentially non-compositional?

Software is composition. Even software that doesn't involve components will ultimately serve as one. For the software that doesn't involve components, I would suggest you should find a better paradigm for said problem than OOP - which is ultimately all about composition of software components.

if you are in charge of a mission-critical development and have to sign as statement that the software is correct, you will want to verify the full thing anyway, not rely blindly on someone else's guarantee that some routine or class is correct

Software composition doesn't require we "rely blindly on someone else's guarantee that some routine or class is correct". Static analyses, auditing, and automated tests of various sorts may, of course, apply. But, for 'large' software, we must ultimately collaborate, communicate, and compose. Communicating to other developers how features interact is just 'interface' or 'protocol' by another name.

For clarity: by 'large' software, I refer to software whose implementation is detailed beyond the comprehension of any single human or group. Issues of incomplete specification, distribution, and upgrade are inherent in such systems. Similarly are issues of interface: describing how components or features interact with one another and their environment.

It is not "wishful thinking" to assert that 'large' software involves composition; that's simply the nature of the beast. If a problem precludes a compositional software solution, you hope it either need not be solved or that it can be solved with a small and complete software specification (such that it may be composed into other systems).

Compositionality

You are right to insist that software construction should be modular and software compositional . The problem is that if we consider existing programming languages (in this case modern object-oriented languages), we are studying an objective reality, much as a natural scientist would do, and have to consider the properties it has rather than the properties we would like it to have.

A property p is compositional if p (o), applied to an object o with components o1 and o2, can be deduced from p (o1) and p (o2), each determined independently of o. Unfortunately aliasing is not compositional in this sense. This is highly regrettable, but once we recover from the pain we can try to harness aliasing anyway, which is what my calculus attempts to do.

Since we are dealing with human artifacts rather than objects of nature, we can (unlike natural scientists) change the reality; this means using programming languages with no aliasing. But if we deal with languages that have aliasing we must accept the facts.