The Racket Virtual Machine and Randomized Testing

• The paper: racket-machine.pdf
• The models: racket-machine.tar.gz
• The README from racket-machine.tar.gz:

  This archive contains the PLT Redex model and tests described in the paper
  _The Racket Virtual Machine and Randomized Testing_.
  
  These files are known to work with Racket v5.0.2, but changes to the
  compiler may break compatibility. Subsequent Racket releases include
  compatible versions in redex-examples pkg.
  
  The archive contains the following files:
  
     == example.rkt: functions for compiling surface-level expressions to
     bytecode, evaluating bytecode, generating reduction graphs, and
     stepping through reductions. Run this program with the command-line
     tool `gracket' or in DrRacket (use the "Use the language declared in
     the source" language).
  
     == grammar.rkt: the bytecode grammar
  
     == reduction.rkt, reduction-test.rkt: the bytecode loader and machine
     transitions
  
     == verification.rkt, verification-test.rkt: the bytecode verifier
  
     == randomized-tests.rkt, randomized-tests-test.rkt: random tests
     checking (1) that the verifier's result is defined for all bytecode,
     (2) that verified programs don't go wrong, (3) that two optimizations
     preserve the meaning of verified programs, and (4) that the machine
     model and implementation agree
  
     == run-tests.rkt: a script for running the tests
  
     == util.rkt: miscellaneous definitions shared by the verifier and
     reduction rules
  
     == impl-eval.rkt, impl-exec.rkt: a function that evaluates bytecode on
     the real machine, using a separate process (in case the bytecode
     crashes or corrupts the machine)
  
     == model-impl.rkt: functions for converting between the model's
     bytecode representation and the implementation's
  
  Note: the expression forms described in the paper differ slightly from
  the ones described in the documentation of the compiler/zo-parse
  module. The following table summarizes the differences in v5.0.2.
  
     [| (loc n) |]                = (localref #f n #f #t #f)
     [| (loc-clr n) |]            = (localref #f n #t #t #f)
     [| (loc-noclr n) |]          = (localref #f n #f #f #f)
     [| (loc-box n) |]            = (localref #t n #f #t #f)
     [| (loc-box-clr n) |]        = (localref #t n #f #t #f)
     [| (loc-box-noclr n) |]      = (localref #t n #f #f #f)
     [| (let-void n e) |]         = (let-void n #f [| e |])
     [| (let-void-box n e) |]     = (let-void n #t [| e |])
     [| (install-value n e e') |] = (install-value 1 n #f [| e |] [| e' |])
     [| (install-value n e e') |] = (install-value 1 n #f [| e |] [| e' |])
     [| (proc-const (τs ...) e |] = (closure (lam (τs ...) [| e |]))
     [| (indirect e) |]           = [| e |]
  
  See model-impl.rkt for the precise correspondence.