Here are the HOL sources for the x86 multiprocessor semantics. To Build ======== It is known to work with (at least) HOL revision 6031, in the recent PolyML port. To build it, first, install PolyML 5.2 from http://sourceforge.net/project/showfiles.php?group_id=148318 with something like the following: wget http://downloads.sourceforge.net/polyml/polyml.5.2.tar.gz?modtime=1214245187&big_mirror=0 tar -zxvf polyml.5.2.tar.gz cd polyml.5.2 ./configure --prefix=/usr make sudo make install (you may need a different prefix, and/or to ensure that your PATH contains the install directory/bin and your LD_LIBRARY_PATH contains the install directory/lib) Then install HOL into a directory HOL-poly with something like: svn co https://hol.svn.sf.net/svnroot/hol/HOL HOL-poly cd HOL-poly poly < tools-poly/smart-configure.sml bin/build -expk -symlink (ignore the mllex error at the end), and ensure that HOL-poly/bin is in your PATH. Add -r6031 after "co" above to get that particular version of HOL. Finally, just type "make" in this directory (this takes around 15min on an Intel Core2 2.4Ghz machine). Contents ======== An automatically typeset version of the definitions --------------------------------------------------- alldoc.ps alldoc.pdf This includes the HOL definitions in the files below, except those marked [*]. The HOL proof scripts are not typeset. The definition of the semantics ------------------------------- x86_coretypesScript.sml core type definitions, shared by the sequential and event-based semantics x86_typesScript.sml types for the event-based semantics: event, event_structure, execution_witness, etc. x86_astScript.sml abstract syntax (AST) for x86 instructions x86_axiomatic_modelScript.sml the x86-cc axiomatic memory model x86_niceness_statementScript.sml the definition of "nice" x86-cc executions x86_seq_monadScript.sml the sequential state state monad type constructor and combinators x86_event_monadScript.sml the event monad type constructor and combinators x86_opsemScript.sml the operational semantics for x86 AST instructions, above one of the monads x86_decoderScript.sml decoding from machine code bytes to x86 AST assembly instructions x86_Script.sml the top level for the sequential semantics x86_programScript.sml the top level for the event semantics The proof that the semantics builds well-formed event structures ---------------------------------------------------------------- x86_event_opsem_wfScript.sml [*] x86_program_event_structure_wfScript.sml [*] The proof that the axiomatic model is equivalent to one restricted to nice executions ------------------------------------------------------------------------------------- tactic.sml [*] x86_niceness_proofScript.sml [*] The data-race-freedom development --------------------------------- x86_sequential_axiomatic_modelScript.sml the definition of sequential execution used in the data-race-freedom development x86_axiomatic_model_thmsScript.sml [*] auxiliary theorems about the axiomatic model, used in the data-race-freedom development x86_drfScript.sml the statements and proof scripts for the main data-race-freedom theorems An abstract machine that corresponds to the axiomatic memory model ------------------------------------------------------------------ x86_hb_machineScript.sml the hb machine definition x86_lts_opsScript.sml auxiliary definitions for operations over labelled transition systems x86_hb_machine_thmsScript.sml statements of theorems about the hb machine, and hand proofs thereof Other auxiliary files --------------------- bit_listScript.sml [*] decoderScript.sml [*] opmonScript.sml [*] utilScript.sml [*] utilLib.sig [*] utilLib.sml [*] HolDoc.sml [*] HolDoc.sig [*] README-spec-public this file LICENSE-spec-public the BSD-style license