Temporary assertion fix

[Sumith1896]

Benchmarking this on simplified-lda.rkt ~gives me no performance benefits~ needs re-doing

[rohinmshah]

Did it reduce the number of valid assertions generated and sent to the solver? How many assertions did it get rid of?

How does this affect permutation.rkt?

[Sumith1896]

I have done some further investigation: for remove-child in swift.rkt without this fix

sumith1896@yoda:~/uwplse/syncro$ time racket debug-swift.rkt 
Number of asserts made 1070
Printing time for filtering out clauses
cpu time: 434436 real time: 863418 gc time: 26908
Num old asserts: 1070
Num new asserts: 854

with this fix

sumith1896@yoda:~/uwplse/syncro$ time racket debug-swift.rkt 
Number of asserts made 1046
Printing time for filtering out clauses
cpu time: 341584 real time: 605017 gc time: 19100
Num old asserts: 1046
Num new asserts: 854

[Sumith1896]

Okay I need to add different structs for all types

[rohinmshah]

Wow, it takes 10 minutes to filter through the clauses? That's... a lot.

Actually I think I know what the issue here is -- as a preprocessing step in the grammar, we monomorphize all of the types (this is done by remove-polymorphism, which I think is in grammar.rkt). So there's a vector-ref with type (Procedure-type (list (Vector-type Word Topic) Word) Topic), which won't match the types you've created. Some possible solutions:

1. Instead of matching on the type, match on the name of the procedure. For example, check that the procedure name is vector-increment! or vector-decrement! and if it is then use the corresponding struct that you defined. This will group together different applications of vector-increment!, but that shouldn't be a big deal -- I think you'll eliminate most of the assertions with this approach.

2. Dynamically generate new struct definitions from a type, and store a type to struct cache.

[rohinmshah]

Oh, also, you are generating fresh type variables, which will not be equal? to the previously defined fresh type variables:

-> (require "src/rosette/types.rkt")
-> (equal? (Type-var) (Type-var))
#f

This is possibly a bad implementation of polymorphism on my part -- I'm not sure how people normally deal with type variables, but the model I'm using is to create fresh type variables all the time that are not equal to each other.

TL;DR is that polymorphism is hard to deal with and ideally you would do something where you can ignore all of the polymorphism.

The benefits that you are currently getting come from the types that don't have polymorphism (arithmetic, and/or, and comparisons).

Both of the solutions I mentioned above should also avoid this problem :)

[Sumith1896]

Thanks a lot @rohinmshah, this clears some things. Let me try the first approach that you suggest.

[Sumith1896]

Trying to match them by names (latest commit) makes it to:

sumith1896@yoda:~/uwplse/syncro$ racket debug-swift.rkt 
Number of asserts made 964
...

(after filtering around 832, closed that terminal by mistake)

[rohinmshah]

Okay, that seems a lot better. Does it speed up permutation.rkt, lda.rkt and simplified-lda.rkt?

[Sumith1896]

Just saw this, I have not benchmarked it (I'm doing it now, it takes some time) but do you know why it still not able to filter over 100 assertions? Is it because it is grouping together different applications of vector-increment!? If so, is this the best we can do?

[Sumith1896]

Two consecutive runs for swift.rkt

sumith1896@yoda:~/uwplse/syncro$ racket debug-swift.rkt 
Number of asserts made 964
Printing time for filtering out clauses
cpu time: 217288 real time: 408323 gc time: 12420
Num old asserts: 964
Num new asserts: 832
#f
sumith1896@yoda:~/uwplse/syncro$ racket debug-swift.rkt 
Number of asserts made 964
Printing time for filtering out clauses
cpu time: 232764 real time: 435273 gc time: 13152
Num old asserts: 964
Num new asserts: 832

seems to have improved slightly doesn't it?

[rohinmshah]

Yeah, it does :) Do you know how long solver time for synthesis takes, if you don't do any filtering? That's the normal use case.

I don't know why it's not filtering out the other 100 assertions. It could be that those are caused by something else altogether. One way to get more intuition about this is to uncomment the line in rosette/rosette/base/core/effects.rkt that prints out errors it squelches:

  (printf "\n\nERROR: ~a\n\n" err)

If you want a stack trace, then you can do

(require (only-in racket/exn exn->string))
(define (rollback/suppress err)
  (printf "\n\nERROR: ~a\n\n" (exn->string err))

Each such error generates a new assertion in Rosette. (However, it may be a necessary assertion, you can't assume that it's safe to filter out every assertion generated here.)

[Sumith1896]

For swift.rkt with -s option without fix

sumith1896@yoda:~/uwplse/syncro$ racket example/swift.rkt -q -p progress -s
Synthesizing update rule for mb upon delta add-child! to graph
Generating the prederivative
Used 113 boolean variables to encode a search space of log size 54
Took 449ms (448 cpu, 24 gc) to generate the prederivative
Creating symbolic program
Used 457 boolean variables to encode a search space of log size 214
Used 595 boolean variables to encode a search space of log size 243
Took 1507ms (1512 cpu, 36 gc) to generate the sketch
Running the prederivative for configuration 1
Took 32ms (32 cpu, 0 gc) to run the prederivative
Running the generated program for configuration 1
Took 1427ms (1428 cpu, 252 gc) to run the postderivative
Completed symbolic generation! Running the solver:
Took 145243ms (32324 cpu, 1444 gc) to solve the formula
Solution found! Generating code:
'(let ()
   (define tmp19730 (* NUM_NODES NUM_NODES))
   (define tmp19731 (vector-ref mb parent))
   (define tmp19733 tmp19730)
   (define tmp19734 (vector-ref mb parent))
   (begin (add-edge! graph parent child))
   (let ()
     (let ()
       (define constant37757 0)
       (define tmp37758 (+ tmp19733 tmp19733))
       (define tmp37759 (vector-ref mb child))
       (define tmp37760 #f)
       (define tmp37761 constant37757)
       (define tmp37762 (vector-ref mb child))
       (define tmp37763 (equal? mb mb))
       (let () (enum-set-add! tmp37759 parent) (enum-set-add! tmp19734 child)))
     (for-enum-set
      ((other-parent (vertex-parents graph child)))
      (let ()
        (let ()
          (define constant55778 0)
          (define tmp55779 constant37757)
          (define tmp55780 (vector-ref mb child))
          (define tmp55781 #f)
          (define tmp55782 (* tmp19733 tmp19733))
          (define tmp55783 (vector-ref mb other-parent))
          (define tmp55784 (equal? graph graph))
          (let ()
            (if #t (enum-set-add! tmp55783 parent) (set! mb mb))
            (if (equal? tmp55783 tmp19731)
              (enum-set-remove! tmp55783 other-parent)
              (enum-set-add! tmp19731 other-parent))))))))
Synthesizing update rule for mb upon delta remove-child! to graph
Generating the prederivative
Used 113 boolean variables to encode a search space of log size 54
Took 386ms (384 cpu, 20 gc) to generate the prederivative
Creating symbolic program
Used 457 boolean variables to encode a search space of log size 214
Used 595 boolean variables to encode a search space of log size 243
Took 1288ms (1292 cpu, 12 gc) to generate the sketch
Running the prederivative for configuration 1
Took 25ms (24 cpu, 0 gc) to run the prederivative
Running the generated program for configuration 1
Took 968ms (968 cpu, 44 gc) to run the postderivative
Completed symbolic generation! Running the solver:
Took 360218ms (40040 cpu, 2484 gc) to solve the formula
No program found to update mb upon delta remove-child! to graph
'(define (add-child! parent child)
   (begin (add-edge! graph parent child))
   (begin
     (let ()
       (define tmp19730 (* NUM_NODES NUM_NODES))
       (define tmp19731 (vector-ref mb parent))
       (define tmp19733 tmp19730)
       (define tmp19734 (vector-ref mb parent))
       (begin (add-edge! graph parent child))
       (let ()
         (let ()
           (define constant37757 0)
           (define tmp37758 (+ tmp19733 tmp19733))
           (define tmp37759 (vector-ref mb child))
           (define tmp37760 #f)
           (define tmp37761 constant37757)
           (define tmp37762 (vector-ref mb child))
           (define tmp37763 (equal? mb mb))
           (let ()
             (enum-set-add! tmp37759 parent)
             (enum-set-add! tmp19734 child)))
         (for-enum-set
          ((other-parent (vertex-parents graph child)))
          (let ()
            (let ()
              (define constant55778 0)
              (define tmp55779 constant37757)
              (define tmp55780 (vector-ref mb child))
              (define tmp55781 #f)
              (define tmp55782 (* tmp19733 tmp19733))
              (define tmp55783 (vector-ref mb other-parent))
              (define tmp55784 (equal? graph graph))
              (let ()
                (if #t (enum-set-add! tmp55783 parent) (set! mb mb))
                (if (equal? tmp55783 tmp19731)
                  (enum-set-remove! tmp55783 other-parent)
                  (enum-set-add! tmp19731 other-parent))))))))))
'(define (remove-child! parent child)
   (begin (remove-edge! graph parent child))
   (begin
     (set! mb
       (build-vector
        NUM_NODES
        (lambda (node)
          (let* ((parents (vertex-parents graph node))
                 (children (vertex-children graph node))
                 (children-list (enum-set->list children))
                 (aunts
                  (if (null? children-list)
                    (enum-make-set NUM_NODES)
                    (apply
                     enum-set-union
                     (map (curry vertex-parents graph) children-list))))
                 (result (enum-set-union parents children aunts)))
            (enum-set-remove! result node)
            result))))))

with this fix

sumith1896@yoda:~/uwplse/syncro$ racket example/swift.rkt -q -p progress -s
Synthesizing update rule for mb upon delta add-child! to graph
Generating the prederivative
Used 113 boolean variables to encode a search space of log size 54
Took 387ms (384 cpu, 8 gc) to generate the prederivative
Creating symbolic program
Used 457 boolean variables to encode a search space of log size 214
Used 595 boolean variables to encode a search space of log size 243
Took 1259ms (1260 cpu, 32 gc) to generate the sketch
Running the prederivative for configuration 1
Took 23ms (24 cpu, 0 gc) to run the prederivative
Running the generated program for configuration 1
Took 991ms (992 cpu, 64 gc) to run the postderivative
Completed symbolic generation! Running the solver:
Took 28412ms (18984 cpu, 728 gc) to solve the formula
Solution found! Generating code:
'(let ()
   (define tmp15413 (vector-ref mb child))
   (define tmp15416 (vector-ref mb parent))
   (define tmp15417 (equal? parent parent))
   (begin (add-edge! graph parent child))
   (let ()
     (let ()
       (define constant33439 0)
       (define tmp33440 (+ constant33439 constant33439))
       (define tmp33441 tmp15413)
       (define tmp33442 #f)
       (define tmp33443 (* constant33439 constant33439))
       (define tmp33444 tmp15416)
       (define tmp33445 (equal? graph graph))
       (let ()
         (enum-set-add! (vector-ref mb parent) child)
         (enum-set-add! tmp15413 parent)))
     (for-enum-set
      ((other-parent (vertex-parents graph child)))
      (let ()
        (let ()
          (define constant51460 0)
          (define tmp51461 (+ tmp33443 tmp33443))
          (define tmp51462 (vector-ref mb child))
          (define tmp51463 (equal? mb mb))
          (define tmp51464 (* NUM_NODES NUM_NODES))
          (define tmp51465 (vector-ref mb child))
          (define tmp51466 (and tmp15417 tmp51463))
          (let ()
            (enum-set-add! (vector-ref mb other-parent) parent)
            (if (enum-set-contains? tmp15416 other-parent)
              (enum-set-remove! tmp15416 parent)
              (enum-set-add! tmp33444 other-parent))))))))
Synthesizing update rule for mb upon delta remove-child! to graph
Generating the prederivative
Used 113 boolean variables to encode a search space of log size 54
Took 362ms (360 cpu, 4 gc) to generate the prederivative
Creating symbolic program
Used 457 boolean variables to encode a search space of log size 214
Used 595 boolean variables to encode a search space of log size 243
Took 1255ms (1256 cpu, 28 gc) to generate the sketch
Running the prederivative for configuration 1
Took 22ms (24 cpu, 4 gc) to run the prederivative
Running the generated program for configuration 1
Took 792ms (792 cpu, 48 gc) to run the postderivative
Completed symbolic generation! Running the solver:
Took 70270ms (16512 cpu, 764 gc) to solve the formula
No program found to update mb upon delta remove-child! to graph
'(define (add-child! parent child)
   (begin (add-edge! graph parent child))
   (begin
     (let ()
       (define tmp15413 (vector-ref mb child))
       (define tmp15416 (vector-ref mb parent))
       (define tmp15417 (equal? parent parent))
       (begin (add-edge! graph parent child))
       (let ()
         (let ()
           (define constant33439 0)
           (define tmp33440 (+ constant33439 constant33439))
           (define tmp33441 tmp15413)
           (define tmp33442 #f)
           (define tmp33443 (* constant33439 constant33439))
           (define tmp33444 tmp15416)
           (define tmp33445 (equal? graph graph))
           (let ()
             (enum-set-add! (vector-ref mb parent) child)
             (enum-set-add! tmp15413 parent)))
         (for-enum-set
          ((other-parent (vertex-parents graph child)))
          (let ()
            (let ()
              (define constant51460 0)
              (define tmp51461 (+ tmp33443 tmp33443))
              (define tmp51462 (vector-ref mb child))
              (define tmp51463 (equal? mb mb))
              (define tmp51464 (* NUM_NODES NUM_NODES))
              (define tmp51465 (vector-ref mb child))
              (define tmp51466 (and tmp15417 tmp51463))
              (let ()
                (enum-set-add! (vector-ref mb other-parent) parent)
                (if (enum-set-contains? tmp15416 other-parent)
                  (enum-set-remove! tmp15416 parent)
                  (enum-set-add! tmp33444 other-parent))))))))))
'(define (remove-child! parent child)
   (begin (remove-edge! graph parent child))
   (begin
     (set! mb
       (build-vector
        NUM_NODES
        (lambda (node)
          (let* ((parents (vertex-parents graph node))
                 (children (vertex-children graph node))
                 (children-list (enum-set->list children))
                 (aunts
                  (if (null? children-list)
                    (enum-make-set NUM_NODES)
                    (apply
                     enum-set-union
                     (map (curry vertex-parents graph) children-list))))
                 (result (enum-set-union parents children aunts)))
            (enum-set-remove! result node)
            result))))))

[rohinmshah]

Wow, that's like 4-6x speedup! I clearly should have prioritized this a long time ago.

[Sumith1896]

Seems like CI is helping :stuck_out_tongue: