suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

refactor benchmark loops for clarity

Browse Source
This commit is contained in:
Burke Fetscher 2014-04-01 15:47:47 -05:00
parent 3746e639ae
commit ea3b5c0742
1 changed files with 51 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

88
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt
View File

@ -21,6 +21,8 @@
enum ordered fixed)) enum ordered fixed))
(define types '()) (define types '())
(define timeout-time (* 5 60 1000)) ;; 5 mins in ms
(define (set-type! arg) (define (set-type! arg)
(define t (string->symbol arg)) (define t (string->symbol arg))
(unless (list? (member t all-types)) (unless (list? (member t all-types))
@ -106,50 +108,62 @@
(thread (thread
(λ () (system (make-cmd n))))))) (λ () (system (make-cmd n)))))))
(struct timeout ())
(struct reached-limit (tries))
(define (run-generations fname verbose? no-errs? get-gen check seconds type) (define (run-generations fname verbose? no-errs? get-gen check seconds type)
(collect-garbage) (collect-garbage)
(define s-time (current-process-milliseconds)) (define s-time (current-process-milliseconds))
(define time-limit (+ s-time (* 1000 seconds)))
(define terms 0) (define terms 0)
(define counterexamples 0) (define counterexamples 0)
(define (tot-time) (- (current-process-milliseconds) s-time))
(let trials-loop ([t 0] (let trials-loop ([t 0]
[g (get-gen)]) [g (get-gen)])
(define t-time (current-process-milliseconds)) (define trial-start-time (current-process-milliseconds))
(let/ec break (define (me-time) (- (current-process-milliseconds) trial-start-time))
(let loop ([i 0]) (match (one-counterexample trial-start-time time-limit
(define tot-time (- (current-process-milliseconds) s-time)) g check fname type)
(cond [(timeout)
[((/ tot-time 1000) . > . seconds) (trials-loop t g)]
(exit-message fname type (+ i terms) tot-time counterexamples)] [(reached-limit tries)
[else (exit-message fname type (+ tries terms) (tot-time) counterexamples)]
(define term (with-timeout (* 5 1000) g [(list tries term)
(λ () (printf "\nTimed out generating a test term in: ~a, ~a\n" (define continue? (update-results (me-time) fname type verbose?))
fname type) (set! counterexamples (add1 counterexamples))
(break (trials-loop t g))))) (when verbose?
(define me-time (- (current-process-milliseconds) t-time)) (printf "~a: counterexample: ~s\n ~s iterations and ~s milliseconds\n"
(define ok? (with-timeout (* 5 1000) (λ () (check term)) fname term tries (me-time)))
(λ () (printf "\nIn ~a, ~a, timed out checking the term: ~s\n" (when no-errs?
fname type term) (printf "!---------------------------------------------------!\n")
(break (trials-loop t g))))) (error 'run-generations "~a: unexpected error on ~s"
(cond fname term))
[(not ok?) (if (and (not first-only)
(set! counterexamples (add1 counterexamples)) (or continue?
(when verbose? (t . < . 5)))
(printf "~a: counterexample: ~s\n ~s iterations and ~s milliseconds\n" (begin
fname term i me-time)) (set! terms (+ tries terms))
(when no-errs? (trials-loop (add1 t) (get-gen)))
(printf "!---------------------------------------------------!\n") (exit-message fname type (+ tries terms) (tot-time) counterexamples))])))
(error 'run-generations "~a: unexpected error on ~s"
fname term)) (define (one-counterexample s-time time-limit generator check fname type)
(define continue? (update-results me-time fname type verbose?)) (let/ec break
(if (and (not first-only) (let loop ([tries 0])
(or continue? (when ((current-process-milliseconds) . > . time-limit)
(t . < . 5))) (break (reached-limit tries)))
(begin (define term (with-timeout (* 5 1000) generator
(set! terms (+ i terms)) (λ () (printf "\nTimed out generating a test term in: ~a, ~a\n"
(trials-loop (add1 t) (get-gen))) fname type)
(exit-message fname type (+ i terms) tot-time counterexamples))] (break (timeout)))))
[else (define ok? (with-timeout (* 5 1000) (λ () (check term))
(loop (add1 i))])]))))) (λ () (printf "\nIn ~a, ~a, timed out checking the term: ~s\n"
fname type term)
(break (timeout)))))
(cond
[(not ok?)
(list tries term)]
[else
(loop (add1 tries))]))))
(define (exit-message file type terms time countxmps) (define (exit-message file type terms time countxmps)
(printf "----------\n~a, ~s\n" file type) (printf "----------\n~a, ~s\n" file type)