This is the course page for Advanced Models and Programs, spring 2009.
Practical and administrative matters
The course starts on January 26, 2006. In the first week, we meet Monday January 26 from 9-12 in Room 4A20, and on Wednesday January 28 from 15-17 in Room 4A20. Following the first week, the plan is as follows:
- Monday 9-12 (Room 4A20)
- Wednesday 13-15 (Room 4A20)
- Wednesday 15-17, exercises (Room 4A54)
The course period is 16 weeks half time (15 ects). The course will consist of five blocks, covering different themes, with weekly lectures and exercises; and a substantial four-week group project within one of the themes, resulting in a project report.
The weekly exercises must be handed in, and at least 9 of the 11 exercises must be approved to pass the course. You are allowed to work in groups to solve the exercises, but each individual student must write his/her solution up individually and hand it in by him/herself.
For the hand-in status, see here.
The project must be done in groups (2-4 persons in each group) and the project report must be presented in an oral exam, where questions may be asked in all themes of the course.
For a list of groups, their projects, and the associated supervisor, see here.
For a an explanation of how to hand in the final project, see this page.
The official course description says:
"The project report must be presented in an oral exam, where questions may be asked in all themes of the course. A single grade is given, based on the project and the oral exam."
"Ekstern censur, [7-trinsskala], B4: Mundtlig eksamen med skriftlige arbejder men uden forberedelsestid ved eksamen."
We allow a total of 15 minutes for project presentation (by the whole group) and feedback followed by 15 minutes of individual examinations of each student. The individual examinations will cover both the project and all other aspects of the course. The official explanation, found at the ITU intranet, says (in Danish):
"Projekter udarbejdet i gruppe afsluttes med en fælles præsentation umiddelbart før afholdelse af eksamen. Denne præstation er ikke en del af eksamen. I skal være opmærksom på at ved den efterfølgende eksamination eksamineres alle gruppemedlemmer i hele gruppeopgaven.
Hvis en mundtlig eksamen tager udgangspunkt i en rapport eller et skriftligt arbejde, som er udarbejdet af flere studerende, må hvert gruppemedlem først være til stede i eksamenslokalet, når gruppemedlemmet selv skal eksamineres."
The oral exam will take place on June 15, 2009, in room 3A12.
The exam schedule can be seen here.
Intended Learning Outcomes
The course has two parts as detailed under course form below - a regular course followed by a project.
After the course, the students are expected to be able to:
- describe relevant concepts within the themes of the course,
- account for the practical applications of the covered constructs, and
- compare selected techniques and constructions within a single of the course themes.
On the basis of the project, the student are expected to be able to:
- apply relevant methods and techniques in the chosen project
- argue for the overall design-decisions in the project, and
- relate project and theory.
The themes covered in the course includes
- Lexing, parsing and compilation: From source code to abstract syntax to stack machine code
- Real and abstract machines
- Higher-order functions
- Program generation, quasi quotations, program specialization
- Continuations: Continuation-passing style, first-class continuations, continuations in web servers
- Static Analysis; in particular, Data-Flow Analysis
- Basics of Concurrency Theory
|05||Mon 26 Jan||LB||ML intro + expression evaluation||Harper Ch. 2-3-4 Slides||Week 1|
|Wed 28 Jan||LB||ML intro + interpretation + compilation||Harper Ch. 5-6-7 Slides|
|06||Mon 2 Feb||LB||ML intro: data types and higher-order functions||Harper Ch. 9-10-11 Slides||Week 2|
|Wed 4 Feb||LB||ML vs OO: the expression problem||Torgersen ECOOP'04 paper|
|07||Mon 9 Feb||PS||Abstract syntax, interpretation and checking; lexing and parsing||Mogensen sections 2.1-2.8 and 3.1-3.6. Sestoft PLC chapters 1-3. Slides||Week 3|
|Wed 11 Feb||PS||Grammar transformations, compilation and stack machines||Coco/R User Manual pages 1-17, 23-29. Sestoft PLC chapters 1-3 and 7.2. Slides|
|08||Mon 16 Feb||PS||Micro-C and pointers||Kernighan and Ritchie chapter 5. Sestoft PLC chapters 6-7. Slides||Week 4|
|Wed 18 Feb||PS||Bytecode, abstract machines, and real machines||Sestoft PLC chapters 10-11. Sestoft: Numeric performance in C, C# and Java. Ecma-335, partition I, section 12.3. Richter, chapter 1. Slides|
|09||Mon 23 Feb||PS||Scheme and multi-stage programs||Dybvig sections 2.1-2.7, 6.1. Sestoft PLC chapter 14. Slides||Week 5|
|Wed 25 Feb||PS||Runtime code generation in a high-performance spreadsheet implementation||Slides||...|
|10||Mon 2 Mar||MR||Continuations||Sestoft PLC chapter 8. Slides||Week 6|
|Wed 4 Mar||MR||CPS interpreters|
|11||Mon 9 Mar||MR||Backtracking and compiling with continuations||Sestoft PLC section 8.9 + Any material linked to below under "On continuations and CPS". Slides||Week 7|
|Wed 11 Mar||MR||Compiling backtracking with continuations. Enumerators and yield blocks in C#|
|12||Mon 16 Mar||MR||First-class continuations. Continuations and web servers.||Section 1, 3, and 4 of Queinnec's article. Slides||Week 8|
|Wed 18 Mar||MR||Continuations and web servers.||...|
|13||Mon 23 Mar||CB||3 hour lecture on Introduction: Undecidability, Static Analysis, Data-Flow Analysis, and Control-Flow Graphs||Slides Lecture Notes Chapters 1, 2, and 5; i.e., pages 3-6 + 15-17.||Week 9|
|Wed 25 Mar||CB||4 hour lecture on "Extraterrestrial Mathematics" (which we need for Data-Flow Analysis)||Slides How to solve recursive equations Lecture Notes Chapter 4; i.e., pages 11-15.|
|14||Mon 30 Mar||CB||3 hour lecture on Data-flow Analyses in practice; we'll study examples.||Slides Lecture Notes Chapter 6; pages 17-19 + 28-32.||presentation|
|Wed 1 Apr||CB||WORKSHOP on Data-flow Analysis (no lecture); we'll be making analyses :-)|
|15||Mon 6 Apr||Easter|
|Wed 8 Apr||Easter|
|16||Mon 13 Apr||Easter|
|Wed 15 Apr||MC||CCS: Syntax and Semantics||Slides & Exercises||Week 11|
|17||Mon 20 Apr||MC||CCS: Equivalences||Slides||Week 12|
|Wed 22 Apr||MC||Bisimulation Exercise Class||Exercises on Equivalences Tool Support||...|
|18||Mon 27 Apr||Projects|
|Wed 29 Apr||Projects|
|19||Mon 4 May||Projects|
|Wed 6 May||Projects|
|20||Mon 11 May||Projects|
|Wed 13 May||Projects|
|21||Mon 18 May||Projects|
|Wed 20 May||Project reports must be handed in no later than 15:00 on Wednesday 20 May|
Literature and materials
On programming in Standard ML
- ML literature: Robert Harper: Programming in Standard ML (draft book)
- Mads Torgersen: The Expression Problem Revisited, in ECOOP'04.
On compilation and abstract machines
- Torben Mogensen: Basics of compiler design
- Coco/R lexer and parser generator, User Manual pages 1-17, 23-28
- Peter Sestoft: Programming Language Concepts, version 0.34, 2006.
- There is a large number of supporting files for the Programming Language Concepts notes.
- Expressions.ATG, lexer and parser specification for simple expressions
- Expressions.cs, interpreter, checker, compiler for simple expressions
- Machine.cs, stack machine to evaluate compiled expressions and execute compiled micro-C programs
- ex1.txt, a tiny "program" in the expression language
- A Makefile for Assignment 4 with Mono and Linux, thanks to Martin Kjeldsen.
- Kernighan & Ritchie: The C Programming Language, 1988, pages 93-110. (About pointers and pointer arithmetics). This will be handed out in paper form.
- MicroC.ATG, lexer and parser specification for micro-C
- MicroC.cs, interpreter, checker and compiler for micro-C
- test-c.zip, a bunch of micro-C test programs and an input file a.in
- Selsort.cs and Selsort.java, programs for Assignment 8
- Ecma-335 Common Language Infrastructure specification, the standardization of Microsoft CLR and Microsoft Intermediate Language, June 2006; the PDF file contains a detailed description of the .NET bytecode instructions
- Jeffrey Richter: CLR via C#, Microsoft Press 2006, pages 3-22.
- Lindholm and Yellin: The Java Virtual Machine specification, Addison-Wesley 1999
- The Intel x86 machine code is described in two documents: Intel® 64 and IA-32 Architectures Software Developer's Manual Volume 2A: Instruction Set Reference, A-M and Volume 2B: Instruction Set Reference, N-Z. Warning: This is more than 1200 pages in total.
- A more compact description of x86 instructions is found in appendix B of the manual for the open source x86 assembler "nasm"
- Assembly programs (x86, for Linux): tryadd.asm and tryfac.asm
- Peter Sestoft: Numeric performance in C, C# and Java, ITU 2009.
- The PLT Scheme/DrScheme system, available for multiple platforms. First time you use it, configure: Language > Choose language > Legacy Languages > Pretty Big. To time evaluation of expression e, evaluate (time e).
- The SCM system by Aubrey Jaffer. Neat and simple system, especially for Linux; slightly more complicated to install under Windows.
- R Kent Dybvig: The Scheme Programming Language, MIT Press 2003
- RTCG2D2.cs, an example of runtime bytecode generation in .NET
On continuations and CPS
- intp-exp-exn.sml (a CPS interpreter for expressions with exceptions), example-exp-exn.txt (single-stepping the evaluation of a small term).
- intp-imp-exn.sml (a CPS interpreter for a language with statements and expressions and with exceptions).
- An interpreter for a variant of Icon: Parser.grm, Lexer.lex, Ast.sml, Main.sml, Icon.sml, and load. (Everything in one zip file.)
- comp-exp-1.sml (a tiny CPS compiler from expressions to C statements), example-comp-exp-1.txt (single-stepping the compilation of some terms).
- A compiler for a variant of Icon: In addition to the files for the interpreter, download Iconcmp.sml. There is a README file here that explains how to use the interpreter and the compiler. More information about this kind of compilation can be found in section 3 of this article.
- C# generators, iterators, and yield statements: See section 8.18 of the Ecma C# Language Specification.
- Christian Queinnec: "Continuations and Web Servers". (We will primarily focus on sections 1, 3, and 4 of the article.)
- The WebServer-Session Simulator (abbreviated WS3) can be found here. It runs under (Petite) Chez Scheme.
On program analysis
- Michael I. Schwartzbach: Lecture Notes on Static Analysis, BRICS research center, Uni. Aarhus.
- Claus Brabrand: How to Solve Recursive Equations (of monotone functions over lattices), ITU, April 3, 2008.
- Robin Milner: A Calculus of Communicating Systems. 1980.
- Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen and Jiri Srba: Reactive Systems: Modelling, Speciﬁcation and Veriﬁcation. 2007. ----- (Chapters 1-2-3)
Course project proposals
Proposed by Peter Sestoft:
- Change the MicroC compiler to generate x86 code in the form of input for the NASM assembler.
- Extend the MicroC compiler to handle more of real C, such as struct types, switch, break, continue, malloc/free.
- Write an interpreter -- in Standard ML, Scheme, Java or C# -- for a substantial subset of the Icon language, or for SETL or another "unusual" language.
- Performance engineering for a managed platform (JVM, .NET) and modern x86 cpus. Consider either numeric intensive code (matrix multiplication), or object-intensive code such as the C5 collection library. Investigate bottlenecks using profiling, and experiment with alternative implementations and target platforms.
- Write a generator of specialized serialization/deserialization methods in C# (to XML or Json).
Proposed by Lars Birkedal:
- Study the type inference problem for Mini ML and solve associated problems by paper and pencil (proving selected properties of the type system and the algorithm by induction).
- Implement the type inference algorithm W for Mini ML.
Proposed by Claus Brabrand:
- Make a Data-Flow Analysis and implement it such that it can analyze (and optimize) programs written in (a subset of) some familiar language (e.g., Java, C#, ...)
- Slide with proposal
Proposed by Andrzej Wasowski:
Proposed by Kasper Østerbye:
- Use of continuations in webservers. We briefly looked at that in the course, but here I suggest to dive in and understand it in detail. And to make an assesment of the performance characteristics of such a solution.
- Dissect a debugger. We can look at the debugging interface to Java, or dissect the Smalltalk debugger.
- Build a Java version of the Squeak "find method" (the tool in which you write an example input/output and it suggest methods that give that result).
- As always, your suggestions are better than mine.
Proposed by Morten Rhiger:
- Implement a CPS transformation: A program that transforms programs in direct style into programs in continuation-passing style. There are various ways to do this, many of which are very elegant. You could also investigate and compare these different CPS transformations.
- Look at ways in which to implement continuation-passing style programs in languages that do not have higher-order functions (such as Java). One simple approach ammounts to representing higher-order functions as first-order data structures. (This approach was outlined on the last two slides for week 8.) Combined with a CPS transformation, such a representation would give a kind of continuation-passing style for Java (which again could support continuation-based webserver applications in Java).
- Implement an interpreter for a language with a realistic mixture of exceptions, local bindings, variables, generators, backtracking, or first-class continuations. (A good example would be to implement an interpreter for a realistic subset of C#.)
- Implement a compiler for a language with a realistic mixture of exceptions, local bindings, variables, generators, backtracking, or first-class continuations. (A particularly interesting approach would be to base this compiler on an interpreter, using the techniques outlined in lecture 7.) The compiler could generate C, homemade bytecode instructions, instructions for the Java Virtual Machine or for Common Language Runtime (e.g., Microsoft's .Net Framework), or something else.
- Investigate different ways to support
yield returnin Java or other languages that do not have first-class continuations. (One approach, suggested by Peter Sestoft, is to implement
yield returnusing threads.)
- Implement a tiny 'real' webserver using continuations in a language that support first-class continuations (for example Scheme or Standard ML of New Jersey).
- Use an existing continuation-based webserver technology (for example the one supplied with the DrScheme/MzScheme system) to implement an larger web application.
Proposed by Marco Carbone:
- (practical) Implement a tool that inputs CCS process and simulates it (you can choose your favourite programming language).
- (semi-theoretical) Model a complex system in CCS and verify some properties with the concurrency workbench.
- (theoretical) Study Hennessy-Milner logic (logical characterisation of bisimilarity).