remove live-in from stochastic & decomposer

Author: mangpo

GA/test-regression.rkt

@@ -87,7 +87,6 @@
 (test 'interp2 "@ @b b! - @b + -" 5
       '((data . 2)) #:sym #f #:prefix "2 b! dup !b a! @+") ;; @ - over + -
 
-#|
 (test 1 "dup drop up a! @ !" 4 '((data . 1) memory) #:sym #t)
 ;;(test 2 "dup drop up a! @+ !" 4 '((data . 1) memory) #:sym #t)
 (test 3 "dup drop up a! ! @" 4 '((data . 1) memory) #:sym #t)
@@ -103,7 +102,7 @@
       #:assume '((<= . 65535) (<= . 65535) (<= . 65535)) #:sym #f)
 (test 'shaf "0 a! !+ !+ push pop dup 1 b! @b and over - 0 b! @b and or push drop pop" 6
       '((data . 2) (return . 1)) #:sym #f)
-|#
+
 #;(test 'complexB "drop 3 and + push drop pop dup 0 b! @b" 10
       '((data . 2)) #:sym #f) ;; very slow
 #;(test 'rrotate "2 b! !b push drop pop 2 b! @b 0 b! !b up b! @b 0 b! @b 2/ 2/ + 65535 and" 8

GA/test-search.rkt

@@ -119,7 +119,6 @@
         ))
 #;(send stoch superoptimize encoded-code 
       (send machine output-constraint '() 2 0) ;; constraint
-      (send machine output-constraint '(a) 4 1) ;; live-in
       "./driver-0" 3600 #f)
 
 ;(require profile)

TODO

@@ -1,21 +1,15 @@
-Performance
-* default mask-in with check (return early)
-- mask-in & mask-in again (ARM)
-- symbolic: provide input or not?
-
 TODO
-* run regression test
-* user don't have to provide live-in for stoch, use result from combine-live too
+* user don't have to provide live-in for stoch, use result from combine-live too [test stoch]
+  - test regression
+- get rid of live-in parser
 
 Correctness
 - how to prevent users from making a mistake on machine description (ins & outs).
   = e.g. putting arg 0 to be output of str# => backward can't find solution.
   = SOLUTION: extract ins & outs from simulator!!!
 
 1. Revisit
-   - (reduce-precesion) in forwardbackward
-   - change "public" to "protected"
-   - remove (debug-inst) in forwardbackward
+   - remove (debug-inst) in forwardbackward & live-in in stoch
    - template
 
 2. May need to override these functions
@@ -26,9 +20,8 @@ Correctness
      = when using parallel driver, printer:compress-state-space
      = config can be use in program-structor, define-arg-type
    - efficient memory access. memory access operates in a granularity of # of bits defined
-   - bit, const => reduce bitwidth
    - update-progstate-ins-load -store
-   - want stact, contact me
+   - want stack, contact me
    - say that (get) & (set) is used for update-live, update-live-backward, and inverse
      (get-arg-ranges) & (get-valid-opcode)
    - #:try-cmp? in enumerator, (try-cmp?) in forwardbackward

arm/run_test.sh

@@ -1,5 +1,5 @@
 for name in p10_nlz_eq_o0 p12_nlz_le_o0 p21_cycle_o0 p22_parity_o0 p23_count_o0 p19_exchange_o0 p11_nlz_lt_o0 p20_next_higher_o0 p24_roundpower_o0 p13_sign_o0 p14_floor_avg_o0 p15_ceil_avg_o0 p16_max_o0 p17_off_right_o0 p18_is_power_o0 p25_smmul_o0 
 do
     echo $name
-    racket optimize.rkt --enum -p -t 150 -c 4 -d $name programs/$name.s
+    racket optimize.rkt --stoch -s -t 30 -c 1 -d $name programs/$name.s
 done

arm/test-search.rkt

@@ -80,7 +80,6 @@
 ;; p25 -O3
 ;; z3: >5 min, java: 9 s
 
-(define livein (send printer encode-live '(0 3)))
 (define constraint (send printer encode-live '(0)))
 
 (define encoded-prefix (send printer encode prefix))
@@ -101,7 +100,6 @@
 
 #;(send stoch superoptimize encoded-code 
       constraint ;; constraint
-      livein ;; live-in
       "./driver-0" 3600 #f)
 
 (send backward synthesize-window

decomposer.rkt

@@ -23,7 +23,7 @@
     ;; The cooperative search tries L, 2L, 3L, 4L
     (define (window-size) (* 2 (len-limit)))
 
-    (define (superoptimize spec constraint live-in name time-limit size
+    (define (superoptimize spec constraint name time-limit size
                            #:prefix [prefix (vector)] #:postfix [postfix (vector)]
 			   #:assume [assumption (send machine no-assumption)]
 			   #:input-file [input-file #f]

llvm/test-search.rkt

@@ -118,7 +118,6 @@ store i32 %1, i32* %2
                       ))
 #;(send stoch superoptimize encoded-code 
       constraint ;; constraint
-      (send printer encode-live (vector '(%2) #t)) ;; live-in
       "./driver-0" 3600)
 
 ;; Step 4: create enumerative search

parallel-driver.rkt

@@ -126,9 +126,8 @@
                      (pretty-display (format "(define encoded-start-code (send printer encode start-code))"))
                      )
                (pretty-display 
-                (format "(send search superoptimize encoded-code ~a ~a \"~a-~a\" ~a ~a #:assume ~a #:input-file ~a #:start-prog ~a #:prefix encoded-prefix #:postfix encoded-postfix)" 
+                (format "(send search superoptimize encoded-code ~a \"~a-~a\" ~a ~a #:assume ~a #:input-file ~a #:start-prog ~a #:prefix encoded-prefix #:postfix encoded-postfix)" 
                         (send printer output-constraint-string live-out)
-                        (send printer output-constraint-string live-in)
                         path id time-limit prog-size 
                         (send printer output-assume-string assume)
                         (if input-file (string-append "\"" input-file "\"") #f)
@@ -182,7 +181,7 @@
         (define cores-enum
           (cond
            [(equal? search-type `enum) cores]
-           [(equal? search-type `hybrid) (floor (* (/ 2 6) cores))] ;;(floor (* (/ 3 6) cores))]
+           [(equal? search-type `hybrid) (floor (* (/ 3 6) cores))] ;;(floor (* (/ 3 6) cores))]
            [else 0]
            ))
         (define cores-solver 

stochastic.rkt

@@ -40,7 +40,7 @@
     (define (inst-copy-with-op x op) (struct-copy inst x [op op]))
     (define (inst-copy-with-args x args) (struct-copy inst x [args args]))
 
-    (define (superoptimize spec constraint this-live-in
+    (define (superoptimize spec constraint 
                            name time-limit size 
                            #:prefix [prefix (vector)]
                            #:postfix [postfix (vector)]
@@ -50,12 +50,47 @@
       (send machine reset-opcode-pool)
       (send machine reset-arg-ranges)
       (send validator adjust-memory-config spec)
-      
-      (set! live-in (send machine progstate->vector this-live-in))
+
+      ;; 1) User-provided live-in
+      ;; (define live-in-user (send machine progstate->vector this-live-in))
+      ;; (for ([x prefix])
+      ;;      (set! live-in-user (send machine update-live live-in x)))
+
+      ;; 2) Combined automatic live-in
+      ;; (define live1 (send validator get-live-in (vector-append spec postfix) constraint))
+      ;; (define live0 (send validator-abst get-live-in (vector-append prefix spec postfix) constraint))
+      ;; (define live0-list (send machine progstate->vector live0))
+
+      ;; (define live1-list-alt live0-list)
+      ;; (for ([x prefix])
+      ;;      (set! live1-list-alt (send machine update-live live1-list-alt x)))
+      ;; (define live1-list (send machine progstate->vector live1))
+      ;; (set! live-in (combine-live live1-list-alt live1-list))
+
+      ;; 3) get-live-in then update-live
+      (define live0 (send validator get-live-in (vector-append prefix spec postfix) constraint))
+      (define live0-list (send machine progstate->vector live0))
+
+      (set! live-in live0-list)
       (for ([x prefix])
            (set! live-in (send machine update-live live-in x)))
-      ;; (unless live-in
-      ;;         (raise "stochastic: live-in at spec cannot be #f"))
+
+      ;; (unless (vector? live-in-user)
+      ;;         (for ([l1 live-in]
+      ;;               [l2 live-in-user])
+      ;;              (cond
+      ;;               [(boolean? l1)
+      ;;                (when (and l2 (not l1))
+      ;;                      (pretty-display `(live-in ,live-in ,live-in-user))
+      ;;                      (raise "done"))]
+      ;;               [else
+      ;;                (for ([ll1 l1]
+      ;;                      [ll2 l2])
+      ;;                     (when (and ll2 (not ll1))
+      ;;                           (pretty-display `(live-in ,live-in ,live-in-user))
+      ;;                           (raise "done")))])))
+                          
+
 
       (send machine analyze-args (vector) spec (vector) live-in constraint)
       (send machine analyze-opcode (vector) spec (vector))