[ACL2(p)] waterfall-parallelism for centaur directory, single-threaded clause-processors

[acl2]

[ACL2(p)] waterfall-parallelism for centaur directory, single-threaded clause-processors

[ragerdl]

From [email protected] on February 19, 2013 09:52:00

Jared and I spoke about this on the phone today, and I'm documenting some of our conversation.

-- clause-processors/witness-cp.lisp seems to be the first main problem, but it's only a call of oracle-eval, which should be thread-safe in practice

-- another workaround is to add (set-waterfall-parallelism nil) to the cert.acl2 files of each centaur directory

-- we could create a version of oracle-eval that doesn't modify "state" but modifies something else (this would be long-term)

-- maybe we can enable waterfall-parallelism for uses of the CP that don't have restrictions and that could be useful (since restrictions are the reason that we employ oracle-eval)

-- bitops/bitsets.lisp seems to be the only place where witness-cp restrictions are used

-- maybe we could modify witness-cp to enable waterfall-parallelism-hacks for the theorem that uses the witness-CP and then disable the hacks afterwards. This would require a ttag, but maybe witness-cp already requires a ttag

-- maybe disable waterfall-parallelism if we detect a CP that needs to modify state (ACL2(p) implementators note: we might be able to do this when we perform our top-level check before we enter the waterfall, but when we check again inside the waterfall [iirc, because of things like computed hints] we should not toggle waterfall parallelism... duh!). This might actually solve the common case, and aside from the required work and other things he'd like to clean up first, Rager likes this idea a lot. Thanks Jared!

[ragerdl]

From [email protected] on February 28, 2013 18:09:09

As of books revision 1562 , all of the books that use clause-processors that modify state and are certifiable without hons have calls of (set-waterfall-parallelism nil) in them. Here are what probably constitutes a lot of these books, as of revision 1562 (the grep command can miss books because of line breaks and comments).

ragerd@corsair:/r/acl2-devel/books$ grep -R "(set-waterfall-parallelism nil)" . --include=.lisp --include=.acl2 --max-count=1
./coi/quantification/quantification.acl2:(set-waterfall-parallelism nil)
./clause-processors/basic-examples.acl2:(set-waterfall-parallelism nil)
./clause-processors/equality.acl2:(set-waterfall-parallelism nil)
./clause-processors/SULFA/books/sat-tests/tutorial.acl2:(set-waterfall-parallelism nil)
./clause-processors/SULFA/books/sat-tests/sudoku.acl2:(set-waterfall-parallelism nil)
./clause-processors/SULFA/books/sat-tests/test-incremental.acl2:(set-waterfall-parallelism nil)
./misc/profiling.acl2:(set-waterfall-parallelism nil)
./parallel/without-waterfall-parallelism.lisp: (er-progn (set-waterfall-parallelism nil)
./parallel/hint-tests.lisp:(make-event (er-progn (set-waterfall-parallelism nil)
./hints/consider-hint-tests.acl2:(set-waterfall-parallelism nil)
./hints/basic-tests.acl2:(set-waterfall-parallelism nil)
./centaur/misc/defapply.lisp:(set-waterfall-parallelism nil) ; for apply-for-ev-cp
./centaur/gl/cert.acl2:(set-waterfall-parallelism nil)
./centaur/tutorial/intro.lisp:(set-waterfall-parallelism nil) ; for below call of def-gl-clause-processor
./centaur/aig/bddify-correct.lisp:(set-waterfall-parallelism nil) ; for defthm aig-bddify-x-weakening-ok-point
./centaur/aignet/aignet-base.lisp:(set-waterfall-parallelism nil) ; currently unknown why we need to disable
./rtl/rel7/support/lib1.delta1/mult-proofs.acl2:(set-waterfall-parallelism nil)
ragerd@corsair:/r/acl2-devel/books$

[ragerdl]

From [email protected] on February 28, 2013 18:11:02

In summary, Sol got rid of the need to modify state from witness-cp (Thanks Sol!). I then went through the centaur books and inserted calls of (set-waterfall-parallelism nil) into the remainder books. Except for centaur/gl, where I disabled waterfall-parallelism in its cert.acl2 file.

Status: Fixed

[ragerdl]

From [email protected] on September 03, 2014 05:34:34

Labels: Type-Task