I have reformatted Dijkstra´s original as it appeared in the 1968 Communications of the ACM paper which includes an appendix not in the typewritten manuscript. The appendix gives more details of the methodology for verifying the design.:
https://drive.google.com/file/d/0B9MgWvi9mywhTkxJQzFoTFppZ3dwNHk4TjJUbjA3LTFhT2dV/view?usp=sharing
And Dijkstra´s notes on Multiprogramming go into yet more detail, giving a nice example of how to work through a problem of devising a mechanism which is more or less GNU Screen:
https://www.cs.utexas.edu/users/EWD/ewd01xx/EWD123.PDF
Here is an outline for another version of the system, with real-time performance guarantees. I was moved to write this by the very impressive way that my Standard ML mock-up of the system works.
https://drive.google.com/file/d/0B9MgWvi9mywhbjg0Q0dYOVFkTmVyR0F1YUJDTjAtUTlENnBr/view?usp=sharing
