Size-Change Termination - eller hvordan man sikrer sig, at et program afvikles efter planen
Gæsteforsker professor Amir Ben-Amram takker af efter 6 mdr.s ophold hos DIKU. Resultat: 2 nye artikler om Size Change Termination og en masse ting at følge op på, når han tager tilbage til Tel Aviv-Yaffo Academic College for at undervise israelske studerende i datalogi og algoritmer.
Hvorfor komme hele vejen til Danmark for at forske i noget så specifikt som Size-Change Termination?
Amir: "Danmark - og i særdeleshed DIKU - har en særlig position på dette område, fordi det var her, for ca. 10 år siden, at de afgørende skridt blev taget til at grundlægge dette forskningsområde."
Size-Change Termination (SCT) har hverken noget med udslettelse eller med programmer, der lukker uautoriseret ned at gøre. Size-Change Termination handler om, hvordan man ved hjælp af logik og matematik kan verificere, at et program afvikles og afsluttes som det skal. Med "Size-Change" sigtes der til, at det er ændringer i størrelsen af en enhed der er udgangspunktet, f.eks. en række filer, der skal gennemløbes. Ved at måle på, om antallet af filer reduceres ifølge planen, kan man udlede, om der sker korrekt afslutning, dvs. "termination".
En af SCT-grundlæggerne, Neil Jones, er stadig aktiv på feltet, og det er derfor helt naturligt for mig at komme til DIKU med jævne mellemrum som fysisk ramme for vort mere end 10 år lange samarbejde om forskning i SCT. Vi mødes, udfordrer hinanden, og går så hver til sit for at tænke videre. Det er en meget frugtbar proces, som forskningmæssigt har givet et godt udbytte, mens jeg har været i Danmark."
Under sit ophold på DIKU har Amir Ben-Amram publiceret to nye artikler om Size-Change Termination (kan ses på Amirs hjemmeside: http://www2.mta.ac.il/~amirben/sct.html.).
I vedlagte artikel (på engelsk) gør Amir status over 10 års forskning i Size-Change Termination.
10 Years Of Size-Change Termination
‘Zune' is a portable music player from Microsoft Corporation. On December 31st, 2008, all Zune devices of a particular model froze. There was no way getting them to work again, other than draining the battery, then recharging it on the following day. The reason was (as you might expect) a software bug related to the special date. But what kind of bug causes a machine to freeze? It is a ‘termination bug' - some process in the system just wouldn't terminate. While the Zune story is a notorious example, termination bugs are only too common. How bad is it when your word-processor freezes just when you were going to save your work?
The importance of verifying the termination of program code was already clear to Alan M. Turing, the pioneer of Computer Science (whose centennial year will be celebrated in 2012). In 1948, Turing advocated, in a conference on programming that programmers should mathematically verify that their program terminate. But it is also Turing who proved (in 1936!) that no algorithm can reliably always tell non-terminating programs from terminating one. This suggested that one cannot hope for this verification to be done automatically, which left the burden with the programmer, and thus it was for years.
However, this situation has been slowly changing, and one important step forward was done at DIKU, in the years 1999-2000, by the research group headed by Prof. Neil D. Jones.
Before that time, Prof. Jones had been working, together with his student Arne Glenstrup, on a certain programming tool (called partial evaluator), and they were trying to come up with algorithms to ensure that this tool will not fall into non-termination. This research led Prof. Jones into thinking about how to verify termination in general. He realized that for a lot of (correct) programs, there is a termination proof which does not require a deep understanding of the program. It is based on tracing the data flow in the program and how the size of these data changes at individual program steps. From such an abstract view of a program, one may be able to argue that it must always terminate. Scientific progress often hinges on finding the right abstraction! Then, one must also be willing to research the abstraction, that is, do basic research.
Together with two DIKU guest researchers, Amir Ben-Amram and Chin-Soon Lee, Prof. Jones presented the paper titled The Size-Change Principle for Program Termination in a conference in January 2001. It did not describe any practical experience: completely theoretical, it explained the idea of the abstraction, but also explained how the termination problem, within this abstraction, is decidable and studied its computational complexity. Questions of this kind had been meaningless before the abstraction!
As a matter of fact, similar techniques (the idea of tracing size-changes, and some of the algorithmic ideas) have been independently invented even earlier by researchers in the field of Logic programming. It was the DIKU publication, however, that made the bold jump to the abstraction, and made the idea accessible to researchers not involved in Logic programming. In fact, the 2001 paper illustrated the idea with a simple first-order functional language, and subsequently, work by the three authors, as well as several other researchers, extended its application to more complex functional languages, high-order functional programs, and imperative languages.
The last decade has seen a fruitful tree of research grow out of the seeds described above. A bibliographic list made by Amir Ben-Amram includes about 50 research papers related directly to size-change termination, ranging from the theoretical to the applied. In fact, Jones, Lee and Ben-Amram all proceeded with studying and expanding the subject, mostly theoretically, but Neil Jones also cooperated on an application of the idea to the ML language (with Damien Sereni from Oxford) and Amir Ben-Amram was recently involved in a project where Java Byte-Code programs were analysed (with Carsten Fuhs and Jürgen Giesl from Aachen and Mike Codish and Igor Gonopolskiy from the Ben-Gurion University, Israel). Other research groups implemented techniques based on the size-change principle in programming environments such as ACL2 and Isabelle, and program analysis tools such as the Java analyser Julia.
Theoretically, the initial ideas were expanded in many ways. Among else, the application of the abstraction has been extended from the basic termination problem to quasi-termination (a variant of termination useful for partial evaluators - the application from which the project initially arose) and to determining how fast the program terminates (analysing its complexity).
For more in-depth information, the reader is encouraged to visit Amir Ben-Amram's web page on SCT.