CertiKOS / Advances in Java

These are the links I gave at the close of yesterday's lecture: two APL-related things that came up last week and I think interesting to look at. CertiKOS: Certified OS Kernels Project: CertiKOS Press Release: Yale News This is a project out of the FLINT group at Yale, building large verified systems. CertiKOS is a … Continue reading CertiKOS / Advances in Java


Lecture 15: The Rust Programming Language

This final APL topic addresses programming for memory safety, and in particular the techniques used in the Rust language. Rust is a fairly recent language, designed for “safe systems programming”: providing low-level precise control for programmers, minimal execution overheads, and promises about correct use of memory and threads. In this short introductory lecture I covered … Continue reading Lecture 15: The Rust Programming Language

Lecture 14: Certifying Correctness

This afternoon's lecture presented ways to take proofs of code properties beyond correctness or safety of specific code into the domain of mobile applications, guarantees of trustworthiness, and complete systems. It's now standard to use digital certificates to authenticate software, providing information about where it comes from. However, this doesn't actually say anything about the … Continue reading Lecture 14: Certifying Correctness

Lecture 13: Practical Tools for Java Correctness

Today's lecture presented two different facilities designed to help write Java code that does the right thing: the Java assert statement; and JML, the Java Modeling Language. Both of these approaches aim to record the programmers' expectations about what code is doing. The most immediate effect of this is that the programmer has to actually … Continue reading Lecture 13: Practical Tools for Java Correctness

Lecture 11: Cautionary Tales in Concurrency

This lecture concludes the set on concurrency with three distinctive challenges for concurrent programming and some possible solutions: lock networks, deadlock, and hand-over-hand locking; priority inversion in thread scheduling; and relaxed memory modelsĀ for modern processor architectures. There was also some discussion of differences between the mailbox communication style in Erlang and channel-based communication in the … Continue reading Lecture 11: Cautionary Tales in Concurrency

Lecture 10: Some Other Approaches to Concurrency

Today's lecture set out some alternative approaches for managing concurrency in programming languages: asynchronous message-passing Actors and the always-upbeat optimistic concurrency of Software Transactional Memory. These are two examples from a wide range of mechanisms in use across many programming languages and applications domains, all of which seek to balance the key concurrency requirements of … Continue reading Lecture 10: Some Other Approaches to Concurrency