; bg.lisp - stobj for background computations (in-package "ACL2") (include-book "unicode/list-fix" :dir :system) (include-book "unicode/rev" :dir :system) (defdoc bg ":Doc-Section BG A stobj for background computations~/ ~c[BG] (for \"background\") is a ~il[stobj] that allows expensive computations to be carried out in other threads. ~c[BG] can be used as a stack or queue. Expensive computations may be \"pushed\" onto the queue (via ~il[bg-push]), and the effect of this is to start executing the expensive computation in some background thread. We also provide a blocking pop (~il[bg-pop]) which can be used to wait for one of these computations to return, and retrieve its value. Our use of a stobj is just a trick to ensure that the contents of the stack are \"off limits\" to functions like ~c[car] and ~c[cdr] during execution. This allows us to store extralogical placeholders in the stobj which are understood by ~c[bg-push] and ~c[bg-pop], and which can never be accessed by other ACL2 functions. ~/ ") (make-event ; The reason for this make-event is subtle. One can potentially exploit ; redundancy to introduce additional accessors for bg-accum "before" it is made ; untouchable. To prevent this, do not allow the stobj to be introduced if ; bg-accum has already been defined. (if (function-symbolp 'bg-accum (w state)) (er soft 'bg "Refusing to allow BG to be redundantly redefined.~%") (value '(defstobj bg (bg-accum)))) :check-expansion t) (defund bg-acc (bg) ":Doc-Section BG Logical contents of the accumulator.~/ In the logic, ~c[(bg-acc bg)] retrieves the contents of all objects that have been pushed onto ~c[BG]'s stack. This function cannot be executed, but our theorems for reasoning about operations such as ~il[bg-push] and ~il[bg-pop] are stated in terms of ~c[bg-acc]. As a convenience, ~c[(bg-acc bg)] is logically said to ~c[list-fix] its argument, so it always returns a ~il[true-listp].~/ " (declare (xargs :non-executable t)) (list-fix (bg-accum bg))) (defund bg-clear (bg) ":Doc-Section BG Erase the contents of the accumulator.~/ Executing ~c[(bg-clear bg)] simply erases any currently pushed values in the accumulator. This is a non-blocking operation and does not need to wait for any threads to complete. David: At the moment this does not have any \"under the hood\" implementation. It would be cool if we could actually have it abort any threads that are still running on behalf of bg. Relevant theorems: ~bv[] (defthm bg-acc-of-bg-clear (equal (bg-acc (bg-clear bg)) nil)) ~ev[] ~/ " (declare (xargs :guard t :stobjs bg)) (update-bg-accum nil bg)) (defund bg-endp (bg) ":Doc-Section BG Determine whether the accumulator is empty.~/ ~c[(bg-endp bg)] may be used to determine if ~c[bg]'s accumulator is empty. This is a non-blocking operation, and it is typically used as the test in recursive functions that are traversing the accumulator via ~il[bg-pop]. Relevant theorems: ~bv[] (defthm bg-endp-redefinition (equal (bg-endp bg) (not (bg-acc bg))) :rule-classes :definition) ~ev[] ~/ " (declare (xargs :guard t :stobjs bg)) (atom (bg-accum bg))) (defund bg-rev (bg) ":Doc-Section BG Reverse the accumulator.~/ ~c[(bg-rev bg)] reverses the contents of the accumulator. This is a non-blocking operation that allows you to treat the accumulator as a queue, even though ~il[bg-push] and ~il[bg-pop] treat it as a stack. Relevant theorems: ~bv[] (defthm bg-acc-of-bg-rev (equal (bg-acc (bg-rev bg)) (rev (bg-acc bg)))) ~ev[]~/ " (declare (xargs :guard t :stobjs bg)) (let ((acc (bg-accum bg))) (update-bg-accum (rev acc) bg))) (defund bg-pop (bg) ":Doc-Section BG Retrieve the result of the most recently pushed computation.~/ ~c[(bg-pop bg)] is the fundamental operation for extracting a value from the accumulator. It attempts to retrieve the first (i.e., most recently pushed) value, blocking if the computation has not been completed. Note that you can use ~il[bg-rev] to reverse the order of the elements, in order to begin processing the oldest computations first. Relevant theorems: ~bv[] (defthm mv-nth-0-of-bg-pop (equal (mv-nth 0 (bg-pop bg)) (car (bg-acc bg)))) (defthm bg-acc-of-mv-nth-1-of-bg-pop (equal (bg-acc (mv-nth 1 (bg-pop bg))) (cdr (bg-acc bg))) ~/ " (declare (xargs :guard t :stobjs bg)) (let* ((acc (bg-accum bg)) (car (if (consp acc) (car acc) nil)) (cdr (if (consp acc) (cdr acc) nil)) (bg (update-bg-accum cdr bg))) (mv car bg))) (defund bg-push-fn (val bg) (declare (xargs :guard t :stobjs bg)) (let* ((acc (bg-accum bg))) (update-bg-accum (cons val acc) bg))) (defmacro bg-push (val bg-stobj) `(bg-push-fn (check-vars-not-free (__bg_obj __bg_proc) ,val) ,bg-stobj)) (add-macro-alias bg-push bg-push-fn) ;; TRICK. Push-untouchable makes it an error to ever try to call bg-data or ;; updata-bg-data directly in a definition, or to even mention them in a ;; theorem. This lets us wall off bg-data behind the interface we've developed ;; above. (push-untouchable bg-accum t) (push-untouchable update-bg-accum t) ;; REASONING. These are the theorems that allow us to carry out all of the ;; reasoning we want. (defthm true-listp-of-bg-acc (true-listp (bg-acc bg)) :rule-classes :type-prescription :hints(("Goal" :in-theory (enable bg-acc)))) (defthm bg-acc-of-bg-clear (equal (bg-acc (bg-clear bg)) nil) :hints(("Goal" :in-theory (enable bg-acc bg-clear)))) (defthm bg-endp-redefinition (equal (bg-endp bg) (not (bg-acc bg))) :rule-classes :definition :hints(("Goal" :in-theory (enable bg-acc bg-endp)))) (defthm bg-acc-of-bg-rev (equal (bg-acc (bg-rev bg)) (rev (bg-acc bg))) :hints(("Goal" :in-theory (enable bg-acc bg-rev)))) (defthm mv-nth-0-of-bg-pop (equal (mv-nth 0 (bg-pop bg)) (car (bg-acc bg))) :rule-classes ((:rewrite) ;; Corollary in case someone is not using tools/mv-nth (:rewrite :corollary (equal (car (bg-pop bg)) (car (bg-acc bg))))) :hints(("Goal" :in-theory (enable bg-acc bg-pop)))) (defthm bg-acc-of-mv-nth-1-of-bg-pop (equal (bg-acc (mv-nth 1 (bg-pop bg))) (cdr (bg-acc bg))) :rule-classes ((:rewrite) ;; Corollary in case someone is not using tools/mv-nth (:rewrite :corollary (equal (bg-acc (cadr (bg-pop bg))) (cdr (bg-acc bg))))) :hints(("Goal" :in-theory (enable bg-acc bg-pop) :expand ((:free (n x) (mv-nth n x)))))) (defthm bg-acc-of-bg-push (equal (bg-acc (bg-push val bg)) (cons val (bg-acc bg))) :hints(("Goal" :in-theory (enable bg-acc bg-push)))) (defttag bg) (progn! (set-raw-mode t) (load (compile-file "stobj-raw.lsp")))