Calculate a dependency graph for a parallel assignment.
(atj-parallel-asg-depgraph vars exprs) → graph
Since Java does not have parallel assignment,
in order to assign the expressions
We go through the variables in order, and for each we construct an association pair for the graph represented as an alist. For each variable, we collect all the variables in the corresponding expression, but we exclude the variable itself and any variable not in the initial set. Thus, we use an auxiliary function that has the unchanging initial set as an additional argument.
Function:
(defun atj-parallel-asg-depgraph-aux (vars exprs all-vars) (declare (xargs :guard (and (string-listp vars) (jexpr-listp exprs) (string-listp all-vars)))) (declare (xargs :guard (= (len vars) (len exprs)))) (let ((__function__ 'atj-parallel-asg-depgraph-aux)) (declare (ignorable __function__)) (b* (((when (endp vars)) nil) (var (car vars)) (expr (car exprs)) (deps (remove-equal var (intersection-equal (jexpr-vars expr) all-vars))) (rest-alist (atj-parallel-asg-depgraph-aux (cdr vars) (cdr exprs) all-vars))) (acons var deps rest-alist))))
Theorem:
(defthm alistp-of-atj-parallel-asg-depgraph-aux (b* ((graph (atj-parallel-asg-depgraph-aux vars exprs all-vars))) (alistp graph)) :rule-classes :rewrite)
Theorem:
(defthm atj-parallel-asg-depgraph-aux-subsetp-vars (b* ((?graph (atj-parallel-asg-depgraph-aux vars exprs all-vars))) (subsetp-equal (alist-keys graph) vars)))
Function:
(defun atj-parallel-asg-depgraph (vars exprs) (declare (xargs :guard (and (string-listp vars) (jexpr-listp exprs)))) (declare (xargs :guard (= (len vars) (len exprs)))) (let ((__function__ 'atj-parallel-asg-depgraph)) (declare (ignorable __function__)) (atj-parallel-asg-depgraph-aux vars exprs vars)))
Theorem:
(defthm alistp-of-atj-parallel-asg-depgraph (b* ((graph (atj-parallel-asg-depgraph vars exprs))) (alistp graph)) :rule-classes :rewrite)
Theorem:
(defthm atj-parallel-asg-depgraph-subsetp-vars (b* ((?graph (atj-parallel-asg-depgraph vars exprs))) (subsetp-equal (alist-keys graph) vars)))