Tuesday, February 21, 2012

Volume with snapshots on hz.cs.berkeley.edu

I just lost maybe 4 hours work by typing "rm **/*>o" instead of "rm **/*.o" (argh...), so I set up a btrfs volume on our machine hz that will snapshot itself every hour. So, move your work into /snappervol/your-username if you want that feature. The backups are stored in /snappervol/.snapshots/SNAPSHOT-NUMBER/snapshot. I made a convenience script to get the latest backed up version of a file,

snapper-latest FILENAME

The snapshots seem pretty space-efficient (i.e. taking a snapshot doesn't waste any space if things don't change).

Thursday, July 7, 2011

synthesizing specialized hybrid value comparisons with Clojure metasketching


Recall that the hybrid value modifications in the backend extend the notion of a variable-value to be in four states:
  • A known constant (this was the only non-hybrid possibility before)
  • A value less than some bound
  • A value greater than some bound
  • An unknown value
    Things currently aren't very optimized. Suppose we have a variable x in the third state, i.e. we know x >= BND, where BND is some positive constant. Then, if we want to compute x > 0, we should return constant-true, not unknown. Similarly, if we multiply two large values, we should get another large value.

    There's a lot of these specialized functions -- one for every operator, and for every comparator we want to know whether it's possible, or known, that e.g. x > y, or whether is possible, denoted maybe. Instead of writing these core and critical specializations by hand, it would be nice to sketch them.

minor debugging option changes

Sorry I don't have a lot of engineering time, but I changed the debug options for printing phases a little, and the code handling it is a little cleaner than before. Sorry for breaking it in the meantime.

First, the relevant options are, as per the help screen "skdev --help:debug",

    --debug-print-passes   Print names of stages and visitors as they execute
 -p,--debug-dump-after     Stages / visitors to dump the program after (comma-sep)
 -P,--debug-dump-before    Stages / visitors to dump the program before (comma-sep)

Monday, April 11, 2011

Python tprint output

SKETCH now supports generating Python files from tprint output. This is useful for localizing synthesis; for example, extracting a read-write sequence from a concrete scan network, so that one can then synthesize a function for mapping the indices. For a simple example, consider the following sketch, that multiplies [1 .. 4] by a constant value.