Lambda the Ultimate

inactiveTopic Region-Based Model Abstraction
started 8/7/2003; 1:26:28 AM - last post 8/7/2003; 11:49:05 AM
Ehud Lamm - Region-Based Model Abstraction  blueArrow
8/7/2003; 1:26:28 AM (reads: 1436, responses: 4)
Region-Based Model Abstraction
Region-Based Model Abstraction.Jakob Rehof, Jeremy Condit, James R. Larus and Sriram K. Rajamani. Microsoft Research Technical Report, MSR-TR-2003-47, August 2003.

We present a new technique for abstracting programs to models suitable for state space exploration (e.g., using a model checker). This abstraction technique is based on a region type system in which regions are interpreted as sets of values. A major benefit of the region abstraction is that it soundly supports aggressive state space reduction and state size reduction in the presence of aliasing without relying on either imprecise global static alias analysis or a large pointer slice of the source program prior to model construction. Region types themselves contain only locally sound alias information; however, our models are globally sound by computing dynamically with region names at model checking time. This technique effectively shifts part of the alias analysis to the model checker and leads to state space reduction as well as enhanced model precision. Region types also provide a flexible framework for adjusting the tradeoff between model precision and performance. We have used these techniques to implement a region-based model compiler for C#.

So you start with a Java-like languasge, with reference semantics, and then work like mad to handle aliasing. Wouldn't choosing a better designed language like Ada be a more productive choice? I think we know how people choose the languages they do research on.

Be that as it may, this is an interesting bit of work that combines techniques from type theory and static analysis with model checking. We are likely to see more and more research combining these radically different approaches. Of course, we will also eventually combine more expressive contracts (as types, perhaps) and blame analysis and produce a more comprehensive framework for achieving software reliability.


Posted to Software-Eng by Ehud Lamm on 8/7/03; 1:33:09 AM

Ken Hirsch - Re: Region-Based Model Abstraction  blueArrow
8/7/2003; 6:56:57 AM (reads: 565, responses: 3)
Could you explain, or point to an explanation, of why Ada is better about aliasing?

Ehud Lamm - Re: Region-Based Model Abstraction  blueArrow
8/7/2003; 7:50:09 AM (reads: 570, responses: 0)
I search for a good link, but couldn't find a useful summary. I don't have the time now (maybe a bit later), but here are a few quick notes.

1. Ada uses value semantics, so x:=y doesn't create aliasing, unless x and y are pointers. This means you usually have less aliasing in your programs.

2. You cannot take the address of variables, unless they have a special attribute. This means that if x is an Integer and y is a pointer to Integer (access to Integer, in Ada-speak), you are certain y doesn't point to x, unless x was explcitly to declared as an aliased variable, thus making this aliasing possible.

3. Ada code uses less poitners than you are used to in C and related languages. The language designers made big effort to remove the need for pointers (in order to make memory usage analysis easier). For example Ada has unconstrained arrays, which enable you to write procedures that accept arrays varying lengths, without the programmer explicitly managing addresses and pointers.

Ehud Lamm - Re: Region-Based Model Abstraction  blueArrow
8/7/2003; 8:08:14 AM (reads: 558, responses: 1)
Concerning aliasing in Ada, you might be interested in the paper by W. Gellerich and E. Plodereder, Parameter-Induced Aliasing in Ada, Ada-Europe'2001, LNCS 2043. Here's a quote from the conclusions:

Our analysis of a large sample of Ada programs conclusively shows that aliasing rarely occurs in real world Ada programs, which may be a contributing factor to the reliability of Ada programs.

Ehud Lamm - Re: Region-Based Model Abstraction  blueArrow
8/7/2003; 11:49:05 AM (reads: 553, responses: 0)
A good place to learn about the Ada language rules concerning things like aliasing is the Annotated Ada 95 Language Reference Manual (AARM).

Some starting points:

Section 6.2 (12) (multiple access paths)

Section 3.10 (9) (see for example 9.l: We considered making more kinds of objects aliased by default...).

3.10.2 (1) Operations of Access Types/Language Design Principles

4.1.2 (8) (on array slices)

You can download the text file of the AARM, and search for the appropriate keywords.