Cache & profiling slow inference rules

Summary

I have code which repeatedly reduces to the first term returned from apply-reduction-relation until no more remain. Sometimes, a term causes a reduction in the list to heavily slow down, and I attempted to write code which automatically determines the reduction responsible.

However, the cache defeats this by making subsequent timing information unreliable. In the following program, J takes 5 seconds to reduce the first time, and then 0 seconds. This is because redex caches the computed output of J.

#lang racket

(require redex/reduction-semantics)

(define (time f)
  (define t0 (current-seconds))
  (f)
  (define t (- (current-seconds) t0))
  t
  )

(define-language L
  [x ::= #t #f]
  )

(define-judgment-form L
  #:mode (J I O)
  [(side-condition ,(sleep 5))
   ----
   (J #t #f)])

(time (λ () (apply-reduction-relation J #t))) ; Outputs 5
(time (λ () (apply-reduction-relation J #t))) ; Outputs 0

Workarounds

There are several workarounds:

• Setting caching-enabled? to #f makes the example program above reliably output 5. However, it appears to change the runtime complexity of my larger model. A reduction that calculated in 10 seconds from a new process didn't finish in 40 minutes with caching disabled.

• By moving the model to a submodule and creating a separate namespace for each run, the caches can be isolated.

(define (run-with-cache-isolation)
  (parameterize ([ current-namespace (make-base-namespace) ])
    (namespace-require 'redex/reduction-semantics)
    (namespace-require '(submod "a.rkt" model))
    (eval '(apply-reduction-relation J #t) (current-namespace))
    ))

I haven't yet tested this on the larger program.

One drawback is that the cache will be empty rather than initialized to the original state. If this is an issue, OS-level tools like taking a core dump could be used to exactly recreate the cache.

Possible solutions

• Each rule in a judgment form or reduction relation could get its own global timer. The timer would be started and stopped while redex is checking whether the rule applies. There could be a function to retrieve the list of names and times.

• The cache could be exposed as a parameter, allowing people to write uninvasive profiling tools by saving and restoring it.

Start with redex/reduction-semantics and the apply-reduction-relation entry point; inspect how caching-enabled? affects repeated reductions and how the cache is held. The issue does not choose between per-rule timers and an exposed cache parameter, so first establish the desired API and evaluate it against the supplied example.