[bitc-dev] State Threading

[Jonathan S. Shapiro]

Let me first give a sense of state threading by example. I'm going to
introduce a new assignment operator "<-" to emphasize which assignments
are legal under state threading.

(let ((x (dup 1:int32)))  ; X is a pointer
   (<- x (+ (deref x) 1)))  ; state threadable

This is a binding because the original binding of 'x' becomes dead at
the moment of assignment. In order for this to be true, the required
rule is:

  The value of X must not be captured or live at the time of assignment.

[As we will see below, this is a bit conservative.]


Thus, if I rewrite the above example as:

(let ((x (dup 1:int32)))
  (let (y x)                 ; y captures x
    (set! x (+ (deref x) 1))))  ; not threadable
 
The "captured at the time of assignment" part is crucial, because the
following code is fine:

(let ((x (dup 1:int32)))
  (let (y x)                 ; y captures x
    ... some non-capturing computation ... )
  .. y not in scope here ..
  (<- x (+ (deref x) 1))))  ; state threadable


(defun (next-even y)
  (let ((x (dup y)))
    (<- x (if (odd? y)
              (+ (deref x) 1)
              (+ (deref x) 2)))))

This is okay because the if legs are mutually exclusive.

(defun (next-even y)
  (let ((x (dup y)))
    (<- x (if (odd? (deref x))
              (+ (deref x) 1)
              (+ (deref x) 2)))))


This is okay because the passing of (deref x) at odd? passes a copy.

(defun (ref-odd? x)
  (odd? (deref x)))

(defun (next-even y)
  (let ((x (dup y)))
    (<- x (if (ref-odd? x)
              (+ (deref x) 1)
              (+ (deref x) 2)))))

This is okay because the capture of x by the call to odd? does not
escape past the (if ...). In fact, it does not escape the expression
that applies ref-odd?

So far, we have established that the rules can be boiled down to capture
analysis. But we must be careful. Consider:

(defun (inc-car ls)
  (case ls
    (null   ls))
    (cons   (set! ls.car (+ ls.car 1)))))

(defun (careful)
  (let ((x (cons 1:(mutable int32) nil))
    (<- x (if (null? x) x (inc-car x)))))

Notice that when all is done, the internals of inc-car are mutating the
outer list IN PLACE. What is very strange is that this is okay, because
the list that is passed as a parameter is effectively dead at the point
of update.

The challenge is to come up with a typing scheme that determine this
sort of deadness. There are several possible approaches in the
literature.

But here is a case that is rather more tricky:

(defstruct (link 'a)
  prev: (mutable (link 'a))
  next: (mutable (link 'a)))

(defun (swapfirst fst:(link 'a))
  (let ((snd  l.next)
        (thrd l.next.next))
    (set! snd.next fst)
    (set! snd.prev fst.prev)
    (set! fst.next thrd)
    (set! fst.pref snd)
    (set! thrd.prev fst)
    (set! fst.prev.next fst)))

(begin
  ; assume x not captured
  (<- x (swapfirst x)

This is okay because (a) x is not captured, therefore fst is not
captured, (b) all steps in SWAPFIRST are therefore bindings - kind of.

Well, no, they aren't bindings at all, and in fact snd and thrd capture
references into the middle of fst. This example is completely okay in
ACL2 and completely disallowed in monads. The question is to understand
why.

I have a sneaking suspicion that the answer here relates to memory
region analysis. What is happening is that all of the pointers involved
can be viewed as being internal to a single object that is rooted at its
outermost referencing pointer. As long as we are operating within this
single region, the updates smell okay to me.

So: can we open some discussion to determine whether this might turn out
to be true? Can we combine region analysis and monads or state
threading?

shap