Tutorial Example

Coordinator
Sep 29, 2009 at 1:59 PM

We will soon start a more exhaustive effort for documentation and the development of tutorial material. For this, I am currently looking for a suitable example that could be used as a running example through a tutorial. Does anybody know (or even has verified) a data structure that would be suitable for such a tutorial? Ideally, it would allow to work gradually from simple to advanced concepts based on the same body of code.

Any ideas?

Sep 30, 2009 at 6:50 AM

Hi Stephan,

to start some discussion on this:

maybe reuse one of the 1970s examples of operating system verification?

E.g. C.A.R. Hoare, "A structured paging system", Computer Journal 16, 209-214 (1973, abstract at http://comjnl.oxfordjournals.org/cgi/content/abstract/16/3/209),

or anything by Per Brinch-Hansen on the SOLO operating system, see http://brinch-hansen.net/papers/ (full-text)

Or use more recent stuff from existing (generally available) OS source code, e.g. include/linux/list.h from the GNU/Linux kernel is rather self-contained once one factors out some macros.

Cheers, Holger