wiki:CIVLmeeting2013

Version 2 (modified by zmanchun, 12 years ago) ( diff )

--

  1. bugs to fix for CIVL:
    • report file not found nicer
    • report concrete # procs in message passing required nicer
    • check args to int div/mod nonnegative
    • check out other uses of "bundle"
  1. SARL: do what Green does:
    • slice
    • persistent storage of cache
    • renaming the variables
  1. Make it easy to specify a dependence relation with a library. Use this in POR. Example: send and recv are independent (usually).
  1. Add scope parameter to $heap? meaning: pointers in this heap never leave scope
  1. Add visitor pattern to model?
  1. No static escape analysis needed -- use dynamic escape analysis, read Matt's FMSD paper
  1. Consider implementing a fence or barrier or other structures as primitives
  1. Examples
    • Get examples from Examples, compile
    • Translate benchmarks from CVT/TASS to CIVL
    • Create a SVN repository for examples (both original code and translation in CIVL)
  1. Find other tools to compare with CIVL
    • e.g. CBMC, DIVINE
Note: See TracWiki for help on using the wiki.