fix performance bug in Redex

The bug was in the way matching worked for lists. Specifically, if
you define a grammar like this one:

  e ::= (- e)
        (- e e)
        integer

and you have a term like this:

  (- (- (- (- (- (- (- 11)))))))

then at each step of matching against 'e', Redex would try both
alternatives, meaning it is attempting 2^n matches (where n is
the number of nested minus signs).

The fix eagerly checks the lengths of the lists and so brings this
back to a linear time matching problem.

(This came up in the delimited continuation model from the paper
 _Constraining Delimited Control with Contracts_, ESOP 2013, altho
 Redex's caching can mask the bad behavior, making this linear
 again in normal uses of that model.)
This commit is contained in:
Robby Findler 2014-03-19 12:56:05 -05:00
parent 98719cb5cf
commit a451fcfa47
2 changed files with 57 additions and 16 deletions

View File

@ -1397,22 +1397,29 @@ See match-a-pattern.rkt for more details
;; match-list/boolean : (listof (union repeat (any hole-info -> boolean))) sexp hole-info -> boolean ;; match-list/boolean : (listof (union repeat (any hole-info -> boolean))) sexp hole-info -> boolean
(define (match-list/boolean patterns exp) (define (match-list/boolean patterns exp)
(let loop ([exp exp] (define has-repeats? (ormap repeat? patterns))
[patterns patterns]) (cond
(cond [(not (list? exp)) #f]
[(null? exp) [(and (not has-repeats?)
(let loop ([patterns patterns]) (not (= (length patterns) (length exp))))
(or (null? patterns) #f]
(and (repeat? (car patterns)) [else
(loop (cdr patterns)))))] (let loop ([exp exp]
[(null? patterns) #f] [patterns patterns])
[(repeat? (car patterns)) (cond
(or (loop exp (cdr patterns)) [(null? exp)
(and ((repeat-pat (car patterns)) (car exp)) (let loop ([patterns patterns])
(loop (cdr exp) patterns)))] (or (null? patterns)
[else (and (repeat? (car patterns))
(and ((car patterns) (car exp)) (loop (cdr patterns)))))]
(loop (cdr exp) (cdr patterns)))]))) [(null? patterns) #f]
[(repeat? (car patterns))
(or (loop exp (cdr patterns))
(and ((repeat-pat (car patterns)) (car exp))
(loop (cdr exp) patterns)))]
[else
(and ((car patterns) (car exp))
(loop (cdr exp) (cdr patterns)))]))]))
;; match-list : (listof (union repeat compiled-pattern)) sexp hole-info -> (union #f (listof bindings)) ;; match-list : (listof (union repeat compiled-pattern)) sexp hole-info -> (union #f (listof bindings))
(define (match-list patterns exp hole-info) (define (match-list patterns exp hole-info)

View File

@ -539,6 +539,40 @@
(term (number_1 6) #:lang L)) (term (number_1 6) #:lang L))
'(5 6))) '(5 6)))
(let ()
;; test to make sure that reasonable short-circuiting is happening
;; when matching lists of differing length to avoid exponential behavior
;; this test is fragile because it is based on cpu times.
;; on my machine, with the bug in place it takes 2000+ msec
;; to run and with the fix it takes 200 or so msec.
(define-language abort-core-lang
(e integer
(- e)
(- e e)))
(define (add-minuses t count)
(let loop ([i count])
(cond
[(zero? i) t]
[else `(- ,(loop (- i 1)))])))
(define-values (answer cpu real gc)
(time-apply
(λ ()
(parameterize ([caching-enabled? #f])
(for ([count (in-range 20)])
(redex-match abort-core-lang
e
(add-minuses 11 count)))))
'()))
(test (< cpu 1000) #t))
; ;
; ;
; ;;; ; ; ;;; ;