[M3devel] Modula-3 TLA Win32 Kernel Threads API Specification by Leslie Lamport

[Daniel Alejandro Benavides D.]

Hi all:

I wanted to share what I have found recently:
http://web.archive.org/web/20010712210213/http://www.research.compaq.com/SRC/personal/lamport/tla/threads/threads.html

I would like to make that for POSIX 1003.4 (original DEC proposal) and post it, would Elegofolks mind to upload the Lamport to CVS tree, I think are important design notes of the Win32 Threads API if at all please let me know if interested.

Alas it's TLA code may be considered m3theory subdirectory of m3kernel

In fact there is a TLA checker written in connection with Zeus Algorithm Animation system for automating the animation of proofs, so I guess we just lack that part for further integration.

Thanks in advance 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://m3lists.elegosoft.com/pipermail/m3devel/attachments/20120707/06740669/attachment-0001.html>