13hannes11 / eldarica Goto Github PK

View Code? Open in Web Editor NEW

This project forked from uuverifiers/eldarica

0.0 0.0 0.0 76.77 MB

The Eldarica model checker

License: Other

Shell 0.48% Smarty 0.05% Scala 57.50% Makefile 0.34% SMT 41.02% Lex 0.38% C 0.22%

eldarica's People

Contributors

Watchers

eldarica's Issues

Deadlock for parallel version

Dump with CTRL + \

   java.lang.Thread.State: WAITING (on object monitor)
	at java.lang.Object.wait([email protected]/Native Method)
	- waiting on <0x0000000085a310c0> (a scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask)
	at java.lang.Object.wait([email protected]/Object.java:328)
	at scala.concurrent.forkjoin.ForkJoinTask.externalAwaitDone(ForkJoinTask.java:295)
	- waiting to re-lock in wait() <0x0000000085a310c0> (a scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask)
	at scala.concurrent.forkjoin.ForkJoinTask.doJoin(ForkJoinTask.java:341)
	at scala.concurrent.forkjoin.ForkJoinTask.join(ForkJoinTask.java:673)
	at scala.collection.parallel.ForkJoinTasks$WrappedTask$class.sync(Tasks.scala:378)
	at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.sync(Tasks.scala:443)
	at scala.collection.parallel.ForkJoinTasks$class.executeAndWaitResult(Tasks.scala:426)
	at scala.collection.parallel.ForkJoinTaskSupport.executeAndWaitResult(TaskSupport.scala:56)
	at scala.collection.parallel.ExecutionContextTasks$class.executeAndWaitResult(Tasks.scala:558)
	at scala.collection.parallel.ExecutionContextTaskSupport.executeAndWaitResult(TaskSupport.scala:80)
	at scala.collection.parallel.ParIterableLike$class.filter(ParIterableLike.scala:596)
	at scala.collection.parallel.mutable.ParArray.filter(ParArray.scala:56)
	at lazabs.horn.bottomup.CEGAR.genAbstractState(CEGAR.scala:848)
	at lazabs.horn.bottomup.CEGAR$$anonfun$genEdge$1.apply(CEGAR.scala:818)
	at lazabs.horn.bottomup.CEGAR$$anonfun$genEdge$1.apply(CEGAR.scala:789)
	at lazabs.horn.bottomup.Hasher.scope(Hasher.scala:380)
	- locked <0x0000000085a97d80> (a lazabs.horn.bottomup.Hasher)
	at lazabs.horn.bottomup.CEGAR.genEdge(CEGAR.scala:789)
	at lazabs.horn.bottomup.CEGAR.liftedTree1$1(CEGAR.scala:164)
	at lazabs.horn.bottomup.CEGAR.<init>(CEGAR.scala:163)
	at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:145)
	at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$28.apply(HornWrapper.scala:424)
	at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$28.apply(HornWrapper.scala:418)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
	at scala.Console$.withOut(Console.scala:65)
	at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:418)
	at lazabs.horn.bottomup.HornWrapper$$anonfun$13.apply(HornWrapper.scala:280)
	at lazabs.horn.bottomup.HornWrapper$$anonfun$13.apply(HornWrapper.scala:282)
	at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
	at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:279)
	at lazabs.horn.Solve$.apply(Solve.scala:81)
	at lazabs.Main$.doMain(Main.scala:632)
	at lazabs.Main$.main(Main.scala:281)
	at lazabs.Main.main(Main.scala)

"Reference Handler" #2 daemon prio=10 os_prio=0 cpu=0,73ms elapsed=12,93s tid=0x00007ff044111000 nid=0xc88 waiting on condition  [0x00007ff0177fe000]
   java.lang.Thread.State: RUNNABLE
	at java.lang.ref.Reference.waitForReferencePendingList([email protected]/Native Method)
	at java.lang.ref.Reference.processPendingReferences([email protected]/Reference.java:241)
	at java.lang.ref.Reference$ReferenceHandler.run([email protected]/Reference.java:213)

"Finalizer" #3 daemon prio=8 os_prio=0 cpu=0,45ms elapsed=12,93s tid=0x00007ff04411b000 nid=0xc89 in Object.wait()  [0x00007ff016476000]
   java.lang.Thread.State: WAITING (on object monitor)
	at java.lang.Object.wait([email protected]/Native Method)
	- waiting on <0x0000000081a01308> (a java.lang.ref.ReferenceQueue$Lock)
	at java.lang.ref.ReferenceQueue.remove([email protected]/ReferenceQueue.java:155)
	- waiting to re-lock in wait() <0x0000000081a01308> (a java.lang.ref.ReferenceQueue$Lock)
	at java.lang.ref.ReferenceQueue.remove([email protected]/ReferenceQueue.java:176)
	at java.lang.ref.Finalizer$FinalizerThread.run([email protected]/Finalizer.java:170)

"Signal Dispatcher" #4 daemon prio=9 os_prio=0 cpu=0,33ms elapsed=12,92s tid=0x00007ff044122000 nid=0xc8a waiting on condition  [0x0000000000000000]
   java.lang.Thread.State: RUNNABLE

"Service Thread" #5 daemon prio=9 os_prio=0 cpu=0,13ms elapsed=12,92s tid=0x00007ff044124000 nid=0xc8b runnable  [0x0000000000000000]
   java.lang.Thread.State: RUNNABLE

"C2 CompilerThread0" #6 daemon prio=9 os_prio=0 cpu=7161,84ms elapsed=12,92s tid=0x00007ff044126000 nid=0xc8c waiting on condition  [0x0000000000000000]
   java.lang.Thread.State: RUNNABLE
   No compile task

"C1 CompilerThread0" #8 daemon prio=9 os_prio=0 cpu=3673,56ms elapsed=12,92s tid=0x00007ff044128000 nid=0xc8d waiting on condition  [0x0000000000000000]
   java.lang.Thread.State: RUNNABLE
   No compile task

"Sweeper thread" #9 daemon prio=9 os_prio=0 cpu=11,52ms elapsed=12,92s tid=0x00007ff04412a000 nid=0xc8e runnable  [0x0000000000000000]
   java.lang.Thread.State: RUNNABLE

"Common-Cleaner" #10 daemon prio=8 os_prio=0 cpu=0,81ms elapsed=12,89s tid=0x00007ff04415d800 nid=0xc90 in Object.wait()  [0x00007fefebffe000]
   java.lang.Thread.State: TIMED_WAITING (on object monitor)
	at java.lang.Object.wait([email protected]/Native Method)
	- waiting on <0x0000000081a019f8> (a java.lang.ref.ReferenceQueue$Lock)
	at java.lang.ref.ReferenceQueue.remove([email protected]/ReferenceQueue.java:155)
	- waiting to re-lock in wait() <0x0000000081a019f8> (a java.lang.ref.ReferenceQueue$Lock)
	at jdk.internal.ref.CleanerImpl.run([email protected]/CleanerImpl.java:148)
	at java.lang.Thread.run([email protected]/Thread.java:829)
	at jdk.internal.misc.InnocuousThread.run([email protected]/InnocuousThread.java:134)

"C2 CompilerThread1" #7 daemon prio=9 os_prio=0 cpu=7074,44ms elapsed=12,17s tid=0x00007feff8158800 nid=0xc94 waiting on condition  [0x0000000000000000]
   java.lang.Thread.State: RUNNABLE
   No compile task

"ForkJoinPool-1-worker-5" #16 daemon prio=5 os_prio=0 cpu=4,86ms elapsed=3,98s tid=0x00007ff0448d7000 nid=0xc9a waiting for monitor entry  [0x00007fefea675000]
   java.lang.Thread.State: BLOCKED (on object monitor)
	at lazabs.horn.bottomup.Hasher.mightBeImplied(Hasher.scala:398)
	- waiting to lock <0x0000000085a97d80> (a lazabs.horn.bottomup.Hasher)
	at lazabs.horn.bottomup.PredicateStore.predIsConsequenceWithHasher(PredicateStore.scala:145)
	at lazabs.horn.bottomup.CEGAR$$anonfun$45.apply(CEGAR.scala:848)
	at lazabs.horn.bottomup.CEGAR$$anonfun$45.apply(CEGAR.scala:848)
	at scala.collection.parallel.mutable.ParArray$ParArrayIterator.filter2combiner_quick(ParArray.scala:435)
	at scala.collection.parallel.mutable.ParArray$ParArrayIterator.filter2combiner(ParArray.scala:426)
	at scala.collection.parallel.ParIterableLike$Filter.leaf(ParIterableLike.scala:1109)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply$mcV$sp(Tasks.scala:49)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48)
	at scala.collection.parallel.Task$class.tryLeaf(Tasks.scala:51)
	at scala.collection.parallel.ParIterableLike$Filter.tryLeaf(ParIterableLike.scala:1105)
	at scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.internal(Tasks.scala:159)
	at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.internal(Tasks.scala:443)
	at scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.compute(Tasks.scala:149)
	at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.compute(Tasks.scala:443)
	at scala.concurrent.forkjoin.RecursiveAction.exec(RecursiveAction.java:160)
	at scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
	at scala.concurrent.forkjoin.ForkJoinTask.doJoin(ForkJoinTask.java:341)
	at scala.concurrent.forkjoin.ForkJoinTask.join(ForkJoinTask.java:673)
	at scala.collection.parallel.ForkJoinTasks$WrappedTask$class.sync(Tasks.scala:378)
	at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.sync(Tasks.scala:443)
	at scala.collection.parallel.ForkJoinTasks$class.executeAndWaitResult(Tasks.scala:426)
	at scala.collection.parallel.ForkJoinTaskSupport.executeAndWaitResult(TaskSupport.scala:56)
	at scala.collection.parallel.ExecutionContextTasks$class.executeAndWaitResult(Tasks.scala:558)
	at scala.collection.parallel.ExecutionContextTaskSupport.executeAndWaitResult(TaskSupport.scala:80)
	at scala.collection.parallel.ParIterableLike$ResultMapping.leaf(ParIterableLike.scala:958)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply$mcV$sp(Tasks.scala:49)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48)
	at scala.collection.parallel.Task$class.tryLeaf(Tasks.scala:51)
	at scala.collection.parallel.ParIterableLike$ResultMapping.tryLeaf(ParIterableLike.scala:953)
	at scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.compute(Tasks.scala:152)
	at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.compute(Tasks.scala:443)
	at scala.concurrent.forkjoin.RecursiveAction.exec(RecursiveAction.java:160)
	at scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
	at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339)
	at scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979)
	at scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107)

"ForkJoinPool-1-worker-3" #17 daemon prio=5 os_prio=0 cpu=0,81ms elapsed=3,98s tid=0x00007fefd400f000 nid=0xc9b waiting for monitor entry  [0x00007fefcfffe000]
   java.lang.Thread.State: BLOCKED (on object monitor)
	at lazabs.horn.bottomup.Hasher.mightBeImplied(Hasher.scala:398)
	- waiting to lock <0x0000000085a97d80> (a lazabs.horn.bottomup.Hasher)
	at lazabs.horn.bottomup.PredicateStore.predIsConsequenceWithHasher(PredicateStore.scala:145)
	at lazabs.horn.bottomup.CEGAR$$anonfun$45.apply(CEGAR.scala:848)
	at lazabs.horn.bottomup.CEGAR$$anonfun$45.apply(CEGAR.scala:848)
	at scala.collection.parallel.mutable.ParArray$ParArrayIterator.filter2combiner_quick(ParArray.scala:435)
	at scala.collection.parallel.mutable.ParArray$ParArrayIterator.filter2combiner(ParArray.scala:426)
	at scala.collection.parallel.ParIterableLike$Filter.leaf(ParIterableLike.scala:1109)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply$mcV$sp(Tasks.scala:49)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48)
	at scala.collection.parallel.Task$$anonfun$tryLeaf$1.apply(Tasks.scala:48)
	at scala.collection.parallel.Task$class.tryLeaf(Tasks.scala:51)
	at scala.collection.parallel.ParIterableLike$Filter.tryLeaf(ParIterableLike.scala:1105)
	at scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask$class.compute(Tasks.scala:152)
	at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.compute(Tasks.scala:443)
	at scala.concurrent.forkjoin.RecursiveAction.exec(RecursiveAction.java:160)
	at scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
	at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339)
	at scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979)
	at scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107)

"VM Thread" os_prio=0 cpu=32,12ms elapsed=12,94s tid=0x00007ff04410e800 nid=0xc87 runnable  

"GC Thread#0" os_prio=0 cpu=90,44ms elapsed=12,95s tid=0x00007ff04402e000 nid=0xc82 runnable  

"GC Thread#1" os_prio=0 cpu=90,75ms elapsed=12,51s tid=0x00007ff00c001000 nid=0xc92 runnable  

"GC Thread#2" os_prio=0 cpu=109,42ms elapsed=12,51s tid=0x00007ff00c002000 nid=0xc93 runnable  

"G1 Main Marker" os_prio=0 cpu=1,03ms elapsed=12,95s tid=0x00007ff044060800 nid=0xc83 runnable  

"G1 Conc#0" os_prio=0 cpu=7,05ms elapsed=12,95s tid=0x00007ff044062000 nid=0xc84 runnable  

"G1 Refine#0" os_prio=0 cpu=0,50ms elapsed=12,95s tid=0x00007ff0440db000 nid=0xc85 runnable  

"G1 Young RemSet Sampling" os_prio=0 cpu=3,70ms elapsed=12,95s tid=0x00007ff0440dc800 nid=0xc86 runnable  
"VM Periodic Task Thread" os_prio=0 cpu=17,49ms elapsed=12,90s tid=0x00007ff04415b000 nid=0xc8f waiting on condition  

JNI global refs: 9, weak refs: 0

Heap
 garbage-first heap   total 163840K, used 9367K [0x0000000081800000, 0x0000000100000000)
  region size 1024K, 7 young (7168K), 6 survivors (6144K)
 Metaspace       used 26228K, capacity 29399K, committed 29952K, reserved 1075200```

Parallelize addFormula

eldarica/src/lazabs/horn/bottomup/Hasher.scala

Lines 245 to 259 in 9bcc056

    
             def addFormula(f : Conjunction) : Int = 
        
               formula2Id.getOrElseUpdate(f, { 
        
                 val res = watchedFormulas.size 
        
                 watchedFormulas += f 
        
                 val evalVector = new MBitSet 
        
                 for (i <- 0 until models.size) 
        
                   if (eval(i, f)) 
        
                     evalVector += i 
        
                 evalVectors += evalVector 
        
           //    println("Adding " + f + ": " + evalVector) 
        
                 res 
        
               })

Do detailed profiling of possible functions to parallelize

Pick random benchmarks from our set of benchmarks (maybe 15) and do profiling with them.

We should add these parts already to the report.

Parallelize part of extendEvalVectors

eldarica/src/lazabs/horn/bottomup/Hasher.scala

Lines 298 to 316 in 9bcc056

    
           private def extendEvalVectors(modelIndex : Int) : Unit = { 
        
             val model = models(modelIndex) 
        
             val assignedConstants = model.constants 
        
             // update the stored vectors 
        
             for (formulaIndex <- 0 until watchedFormulas.size) { 
        
               val formula = watchedFormulas(formulaIndex) 
        
               val vector = evalVectors(formulaIndex) 
        
               val newBit = 
        
                 if (Seqs.disjoint(formula.constants, assignedConstants)) 
        
                   // use existing model where all constants are assigned 0 
        
                   vector(0) 
        
                 else 
        
                   eval(modelIndex, formula) 
        
               setBit(vector, modelIndex, newBit) 
        
             } 
        
           }

Parallelize and just take first model that was found

eldarica/src/lazabs/horn/bottomup/Hasher.scala

Lines 264 to 292 in 9bcc056

    
             def addModel(model : Model) : Unit = { 
        
           //    println("Adding model ...") 
        
               var i = presetModelNum 
        
               var finished = false 
        
               while (i < models.size && !finished) 
        
                 mergeModels(i, model) match { 
        
                   case Some(mergedModel) => { 
        
                     val changedConstants = model.constants filterNot models(i).constants 
        
                     models(i) = mergedModel 
        
                     reducers(i) = ReduceWithConjunction(mergedModel, globalOrder, reducerSettings) 
        
           //    println("Merged with #" + i) 
        
                     extendModelAndUpdateVectors(i, changedConstants) 
        
                     finished = true 
        
                   } 
        
                   case None => 
        
                     i = i + 1 
        
                 } 
        
               if (!finished) { 
        
                 i = models.size 
        
                 models += model 
        
                 reducers += ReduceWithConjunction(model, globalOrder, reducerSettings) 
        
                 extendEvalVectors(i) 
        
           //println("now have " + models.size + " models") 
        
               } 
        
               updateAssertionStack(i) 
        
             }

Updating things are not done in function merge models.

Find matching model in paralell
After match abort run of all threads and call extendModelAndUpdateVectors

Move Hasher into two classses

Stacks need to be updated after models are added (this can be done when we are finished with one round of predicate check genAbstractState?!) might be in is_valid function

What to put in which class:

Assertion Stack Handler
- everything below line 69?!
Hasher
- addFormula, addModel

addModel could have model buffer instead of models directly

We can use internal class for profiling -> aputilTimer.measure("name")
This should be used to figure out which parts of the hasher take the most time.

Possible to parallelize

eldarica/src/lazabs/horn/bottomup/Hasher.scala

Line 250 in 9bcc056

val evalVector = new MBitSet

look into parallelizing isValid

eldarica/src/lazabs/horn/bottomup/HornPredAbsContext.scala

Lines 181 to 211 in 9bcc056

    
           def isValid(prover : ModelSearchProver.IncProver) : Boolean = 
        
             prover.isObviouslyValid || 
        
             Timeout.withChecker(lazabs.GlobalParameters.get.timeoutChecker) { 
        
               hardValidityCheckNum = hardValidityCheckNum + 1 
        
               if (hardValidityCheckNum == hardValidityCheckThreshold) { 
        
                 hardValidityCheckNum = 0 
        
                 hardValidityCheckThreshold = hardValidityCheckThreshold + 2 
        
                 hardValidityCheckNumSqrt = hardValidityCheckNumSqrt + 1 
        
               } 
        
               if (hasher.acceptsModels && (rand nextInt hardValidityCheckNumSqrt) == 0) 
        
                 (prover checkValidity true) match { 
        
                   case Left(m) => 
        
                     if (m.isFalse) { 
        
                       true 
        
                     } else { 
        
                       hasher addModel m 
        
                       false 
        
                     } 
        
                   case Right(_) => 
        
                     throw new Exception("Unexpected prover result") 
        
                 } 
        
               else 
        
                 !prover.isObviouslyUnprovable && 
        
                  ((prover checkValidity false) match { 
        
                     case Left(m) if (m.isFalse) => true 
        
                     case Left(_) => false 
        
                     case Right(_) => 
        
                       throw new Exception("Unexpected prover result") 
        
                   }) 
        
             }

Call genEdge in parallel

eldarica/src/lazabs/horn/bottomup/CEGAR.scala

Lines 165 to 207 in 9bcc056

    
           try { 
        
             for (e <- genEdge(clause, states, assumptions)) 
        
               addEdge(e) 
        
           } catch { 
        
             case Counterexample(from, clause) => { 
        
               // we might have to process this case again, since 
        
               // the extracted counterexample might not be the only one 
        
               // leading to this abstract state 
        
               nextToProcess.enqueue(states, clause, assumptions) 
        
               val clauseDag = extractCounterexample(from, clause) 
        
               iterationNum = iterationNum + 1 
        
               if (lazabs.GlobalParameters.get.log) { 
        
              println 
        
                 print("Found counterexample #" + iterationNum + ", refining ... ") 
        
                 if (lazabs.GlobalParameters.get.logCEX) { 
        
                   println 
        
                   clauseDag.prettyPrint 
        
                 } 
        
               } 
        
               { 
        
                 val predStartTime = System.currentTimeMillis 
        
                 val preds = predicateGenerator(clauseDag) 
        
                 predicateGeneratorTime = 
        
                   predicateGeneratorTime + System.currentTimeMillis - predStartTime 
        
                 preds 
        
               } match { 
        
                 case Right(trace) => { 
        
                   if (lazabs.GlobalParameters.get.log) 
        
                     print(" ... failed, counterexample is genuine") 
        
                   val clauseMapping = normClauses.toMap 
        
                   res = Right(for (p <- trace) yield (p._1, clauseMapping(p._2))) 
        
                 } 
        
                 case Left(newPredicates) => { 
        
                   if (lazabs.GlobalParameters.get.log) 
        
                     println(" ... adding predicates:") 
        
                   addPredicates(newPredicates) 
        
                 } 
        
               } 
        
             }

Define own abstract data type with three option: None, Counterexample, Edge

Challanges

genAbstractState might not be thread safe or make synchronized or move out of genEdge function. (maybe call genAbstractState later on)

Parallelize FindPreStates

eldarica/src/lazabs/horn/bottomup/CEGAR.scala

Lines 521 to 539 in 9bcc056

    
             def findPreStates(i : Int, 
        
                               chosenStates : List[AbstractState], 
        
                               assumptions : Conjunction) : Unit = 
        
               if (i < 0) { 
        
                 nextToProcess.enqueue(chosenStates, clause, assumptions) 
        
               } else if (i == fixedIndex) { 
        
                 findPreStates(i - 1, fixedState :: chosenStates, assumptions) 
        
               } else { 
        
                 val (_, occ) = body(i) 
        
                 for (state <- byStates(i)) { 
        
                   val newAssumptions = 
        
                     sf.reduce(conj(List(assumptions) ++ (state instances occ))) 
        
                   if (!newAssumptions.isFalse) 
        
                     findPreStates(i - 1, state :: chosenStates, newAssumptions) 
        
                 } 
        
               } 
        
             findPreStates(body.size - 1, List(), initialAssumptions) 
        
           }

Parallelize match ClauseSimple

eldarica/src/lazabs/horn/bottomup/CEGAR.scala

Lines 511 to 539 in 9bcc056

    
           def matchClauseSimple(fixedState : AbstractState, 
        
                                 initialAssumptions : Conjunction, 
        
                                 clause : NormClause, 
        
                                 fixedIndex : Int, occ : Int, 
        
                                 byStates : Array[Seq[AbstractState]]) : Unit = { 
        
             import TerForConvenience._ 
        
             implicit val _ = clause.order 
        
             val NormClause(constraint, body, head) = clause 
        
             def findPreStates(i : Int, 
        
                               chosenStates : List[AbstractState], 
        
                               assumptions : Conjunction) : Unit = 
        
               if (i < 0) { 
        
                 nextToProcess.enqueue(chosenStates, clause, assumptions) 
        
               } else if (i == fixedIndex) { 
        
                 findPreStates(i - 1, fixedState :: chosenStates, assumptions) 
        
               } else { 
        
                 val (_, occ) = body(i) 
        
                 for (state <- byStates(i)) { 
        
                   val newAssumptions = 
        
                     sf.reduce(conj(List(assumptions) ++ (state instances occ))) 
        
                   if (!newAssumptions.isFalse) 
        
                     findPreStates(i - 1, state :: chosenStates, newAssumptions) 
        
                 } 
        
               } 
        
             findPreStates(body.size - 1, List(), initialAssumptions) 
        
           }

More benchmarks

https://github.com/chc-comp

Parallelize matchClausePrereduce

eldarica/src/lazabs/horn/bottomup/CEGAR.scala

Lines 543 to 662 in 9bcc056

    
             def matchClausePrereduce(state : AbstractState, 
        
                                      initialAssumptions : Conjunction, 
        
                                      clause : NormClause, 
        
                                      fixedIndex : Int, occ : Int, 
        
                                      byStates : Array[Seq[AbstractState]]) : Unit = { 
        
               import TerForConvenience._ 
        
               implicit val _ = clause.order 
        
               val NormClause(constraint, body, head) = clause 
        
               val relevantRS = 
        
                 (for (p@(t, i) <- body.iterator.zipWithIndex; 
        
                       if (i != fixedIndex)) yield p).toSeq.sortBy { 
        
                   case (_, i) => byStates(i).size 
        
                 } 
        
               var currentAssumptions = initialAssumptions 
        
               var preReducer = sf reducer currentAssumptions 
        
               var foundInconsistency = false 
        
               val availableStates = 
        
                 (for (((rs, occ), i) <- relevantRS.iterator; if (!foundInconsistency)) yield { 
        
                    val states = 
        
                      (for (s <- byStates(i).iterator; 
        
                            simp = preReducer(s predConjunction occ); 
        
                            if (!simp.isFalse)) yield (s, simp)).toArray 
        
                    if (states.isEmpty) { 
        
                      foundInconsistency = true 
        
                    } else if (states.size == 1) { 
        
                      currentAssumptions = sf reduce conj(List(currentAssumptions, states(0)._2)) 
        
                      if (currentAssumptions.isFalse) 
        
                        foundInconsistency = true 
        
                      else 
        
                        preReducer = sf reducer currentAssumptions 
        
                    } 
        
                    (states, i) 
        
                  }).toArray 
        
               if (foundInconsistency) 
        
                 return 
        
           /* 
        
               { 
        
                 val tableSize = body.size 
        
                 val statesTable = 
        
                   Array.ofDim[Array[(List[AbstractState], Conjunction)]](tableSize) 
        
                 statesTable(fixedIndex) = Array((List(state), Conjunction.TRUE)) 
        
                 for ((x, i) <- availableStates) 
        
                   statesTable(i) = for ((s, simp) <- x) yield (List(s), simp) 
        
                 var stride = 1 
        
                 while (2 * stride < tableSize) { 
        
                   var index = 0 
        
                   while (index + stride < tableSize) { 
        
                     val states1 = statesTable(index) 
        
                     val states2 = statesTable(index + stride) 
        
                     statesTable(index) = 
        
                       (for ((s1, simp1) <- states1.iterator; 
        
                             (s2, simp2) <- states2.iterator; 
        
                             simp = 
        
                               if (simp1.isTrue) 
        
                                 simp2 
        
                               else if (simp2.isTrue) 
        
                                 simp1 
        
                               else 
        
                                 preReducer(conj(List(simp1, simp2))); 
        
                             if (!simp.isFalse)) 
        
                        yield (s1 ++ s2, simp)).toArray 
        
                     index = index + 2 * stride 
        
                   } 
        
                   stride = stride * 2 
        
                 } 
        
                 for ((chosenStates1, simp1) <- statesTable(0); 
        
                      (chosenStates2, simp2) <- statesTable(stride)) { 
        
                   val allAssumptions = 
        
                     sf.reduce(conj(List(currentAssumptions, simp1, simp2))) 
        
                   if (!allAssumptions.isFalse) { 
        
                     val allChosenStates = chosenStates1 ++ chosenStates2 
        
                     nextToProcess.enqueue(allChosenStates, clause, allAssumptions) 
        
                   } 
        
                 } 
        
               } 
        
           */ 
        
               Sorting.stableSort(availableStates, 
        
                                  (x : (Array[(AbstractState, Conjunction)], Int)) => x._1.size) 
        
               val chosenStates = Array.ofDim[AbstractState](clause.body.size) 
        
               chosenStates(fixedIndex) = state 
        
               val N = availableStates.size 
        
               def findPreStates(i : Int, 
        
                                 assumptions : Conjunction) : Unit = 
        
                 if (i == N) { 
        
                   val cs = chosenStates.toList 
        
                   nextToProcess.enqueue(cs, clause, assumptions) 
        
                 } else { 
        
                   val (candidates, bodyNum) = availableStates(i) 
        
                   if (candidates.size == 1) { 
        
                     // the constraint has already been taken into account 
        
                     chosenStates(bodyNum) = candidates(0)._1 
        
                     findPreStates(i + 1, assumptions) 
        
                   } else { 
        
                     for ((state, simpStatePreds) <- candidates) { 
        
                       val newAssumptions = 
        
                         sf.reduce(conj(List(assumptions, simpStatePreds))) 
        
                       if (!newAssumptions.isFalse) { 
        
                         chosenStates(bodyNum) = state 
        
                         findPreStates(i + 1, newAssumptions) 
        
                       } 
        
                     } 
        
                   } 
        
                 } 
        
               findPreStates(0, currentAssumptions) 
        
             }

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.

	def addFormula(f : Conjunction) : Int =
	formula2Id.getOrElseUpdate(f, {
	val res = watchedFormulas.size
	watchedFormulas += f

	val evalVector = new MBitSet
	for (i <- 0 until models.size)
	if (eval(i, f))
	evalVector += i
	evalVectors += evalVector

	// println("Adding " + f + ": " + evalVector)

	res
	})

	private def extendEvalVectors(modelIndex : Int) : Unit = {
	val model = models(modelIndex)
	val assignedConstants = model.constants

	// update the stored vectors
	for (formulaIndex <- 0 until watchedFormulas.size) {
	val formula = watchedFormulas(formulaIndex)
	val vector = evalVectors(formulaIndex)

	val newBit =
	if (Seqs.disjoint(formula.constants, assignedConstants))
	// use existing model where all constants are assigned 0
	vector(0)
	else
	eval(modelIndex, formula)

	setBit(vector, modelIndex, newBit)
	}
	}

	def addModel(model : Model) : Unit = {
	// println("Adding model ...")
	var i = presetModelNum
	var finished = false

	while (i < models.size && !finished)
	mergeModels(i, model) match {
	case Some(mergedModel) => {
	val changedConstants = model.constants filterNot models(i).constants
	models(i) = mergedModel
	reducers(i) = ReduceWithConjunction(mergedModel, globalOrder, reducerSettings)
	// println("Merged with #" + i)
	extendModelAndUpdateVectors(i, changedConstants)
	finished = true
	}
	case None =>
	i = i + 1
	}

	if (!finished) {
	i = models.size
	models += model
	reducers += ReduceWithConjunction(model, globalOrder, reducerSettings)
	extendEvalVectors(i)
	//println("now have " + models.size + " models")
	}

	updateAssertionStack(i)
	}

	def isValid(prover : ModelSearchProver.IncProver) : Boolean =
	prover.isObviouslyValid \|\|
	Timeout.withChecker(lazabs.GlobalParameters.get.timeoutChecker) {
	hardValidityCheckNum = hardValidityCheckNum + 1
	if (hardValidityCheckNum == hardValidityCheckThreshold) {
	hardValidityCheckNum = 0
	hardValidityCheckThreshold = hardValidityCheckThreshold + 2
	hardValidityCheckNumSqrt = hardValidityCheckNumSqrt + 1
	}

	if (hasher.acceptsModels && (rand nextInt hardValidityCheckNumSqrt) == 0)
	(prover checkValidity true) match {
	case Left(m) =>
	if (m.isFalse) {
	true
	} else {
	hasher addModel m
	false
	}
	case Right(_) =>
	throw new Exception("Unexpected prover result")
	}
	else
	!prover.isObviouslyUnprovable &&
	((prover checkValidity false) match {
	case Left(m) if (m.isFalse) => true
	case Left(_) => false
	case Right(_) =>
	throw new Exception("Unexpected prover result")
	})
	}

	try {
	for (e <- genEdge(clause, states, assumptions))
	addEdge(e)
	} catch {
	case Counterexample(from, clause) => {
	// we might have to process this case again, since
	// the extracted counterexample might not be the only one
	// leading to this abstract state
	nextToProcess.enqueue(states, clause, assumptions)

	val clauseDag = extractCounterexample(from, clause)
	iterationNum = iterationNum + 1

	if (lazabs.GlobalParameters.get.log) {
	println
	print("Found counterexample #" + iterationNum + ", refining ... ")

	if (lazabs.GlobalParameters.get.logCEX) {
	println
	clauseDag.prettyPrint
	}
	}

	{
	val predStartTime = System.currentTimeMillis
	val preds = predicateGenerator(clauseDag)
	predicateGeneratorTime =
	predicateGeneratorTime + System.currentTimeMillis - predStartTime
	preds
	} match {
	case Right(trace) => {
	if (lazabs.GlobalParameters.get.log)
	print(" ... failed, counterexample is genuine")
	val clauseMapping = normClauses.toMap
	res = Right(for (p <- trace) yield (p._1, clauseMapping(p._2)))
	}
	case Left(newPredicates) => {
	if (lazabs.GlobalParameters.get.log)
	println(" ... adding predicates:")
	addPredicates(newPredicates)
	}
	}
	}

	def findPreStates(i : Int,
	chosenStates : List[AbstractState],
	assumptions : Conjunction) : Unit =
	if (i < 0) {
	nextToProcess.enqueue(chosenStates, clause, assumptions)
	} else if (i == fixedIndex) {
	findPreStates(i - 1, fixedState :: chosenStates, assumptions)
	} else {
	val (_, occ) = body(i)
	for (state <- byStates(i)) {
	val newAssumptions =
	sf.reduce(conj(List(assumptions) ++ (state instances occ)))
	if (!newAssumptions.isFalse)
	findPreStates(i - 1, state :: chosenStates, newAssumptions)
	}
	}

	findPreStates(body.size - 1, List(), initialAssumptions)
	}

	def matchClauseSimple(fixedState : AbstractState,
	initialAssumptions : Conjunction,
	clause : NormClause,
	fixedIndex : Int, occ : Int,
	byStates : Array[Seq[AbstractState]]) : Unit = {
	import TerForConvenience._
	implicit val _ = clause.order

	val NormClause(constraint, body, head) = clause

	def findPreStates(i : Int,
	chosenStates : List[AbstractState],
	assumptions : Conjunction) : Unit =
	if (i < 0) {
	nextToProcess.enqueue(chosenStates, clause, assumptions)
	} else if (i == fixedIndex) {
	findPreStates(i - 1, fixedState :: chosenStates, assumptions)
	} else {
	val (_, occ) = body(i)
	for (state <- byStates(i)) {
	val newAssumptions =
	sf.reduce(conj(List(assumptions) ++ (state instances occ)))
	if (!newAssumptions.isFalse)
	findPreStates(i - 1, state :: chosenStates, newAssumptions)
	}
	}

	findPreStates(body.size - 1, List(), initialAssumptions)
	}

	def matchClausePrereduce(state : AbstractState,
	initialAssumptions : Conjunction,
	clause : NormClause,
	fixedIndex : Int, occ : Int,
	byStates : Array[Seq[AbstractState]]) : Unit = {
	import TerForConvenience._
	implicit val _ = clause.order

	val NormClause(constraint, body, head) = clause

	val relevantRS =
	(for (p@(t, i) <- body.iterator.zipWithIndex;
	if (i != fixedIndex)) yield p).toSeq.sortBy {
	case (_, i) => byStates(i).size
	}

	var currentAssumptions = initialAssumptions
	var preReducer = sf reducer currentAssumptions

	var foundInconsistency = false
	val availableStates =
	(for (((rs, occ), i) <- relevantRS.iterator; if (!foundInconsistency)) yield {
	val states =
	(for (s <- byStates(i).iterator;
	simp = preReducer(s predConjunction occ);
	if (!simp.isFalse)) yield (s, simp)).toArray
	if (states.isEmpty) {
	foundInconsistency = true
	} else if (states.size == 1) {
	currentAssumptions = sf reduce conj(List(currentAssumptions, states(0)._2))
	if (currentAssumptions.isFalse)
	foundInconsistency = true
	else
	preReducer = sf reducer currentAssumptions
	}
	(states, i)
	}).toArray

	if (foundInconsistency)
	return

	/*
	{
	val tableSize = body.size
	val statesTable =
	Array.ofDim[Array[(List[AbstractState], Conjunction)]](tableSize)
	statesTable(fixedIndex) = Array((List(state), Conjunction.TRUE))

	for ((x, i) <- availableStates)
	statesTable(i) = for ((s, simp) <- x) yield (List(s), simp)

	var stride = 1
	while (2 * stride < tableSize) {
	var index = 0
	while (index + stride < tableSize) {
	val states1 = statesTable(index)
	val states2 = statesTable(index + stride)
	statesTable(index) =
	(for ((s1, simp1) <- states1.iterator;
	(s2, simp2) <- states2.iterator;
	simp =
	if (simp1.isTrue)
	simp2
	else if (simp2.isTrue)
	simp1
	else
	preReducer(conj(List(simp1, simp2)));
	if (!simp.isFalse))
	yield (s1 ++ s2, simp)).toArray
	index = index + 2 * stride
	}
	stride = stride * 2
	}

	for ((chosenStates1, simp1) <- statesTable(0);
	(chosenStates2, simp2) <- statesTable(stride)) {
	val allAssumptions =
	sf.reduce(conj(List(currentAssumptions, simp1, simp2)))
	if (!allAssumptions.isFalse) {
	val allChosenStates = chosenStates1 ++ chosenStates2
	nextToProcess.enqueue(allChosenStates, clause, allAssumptions)
	}
	}
	}
	*/

	Sorting.stableSort(availableStates,
	(x : (Array[(AbstractState, Conjunction)], Int)) => x._1.size)

	val chosenStates = Array.ofDim[AbstractState](clause.body.size)
	chosenStates(fixedIndex) = state

	val N = availableStates.size

	def findPreStates(i : Int,
	assumptions : Conjunction) : Unit =
	if (i == N) {
	val cs = chosenStates.toList
	nextToProcess.enqueue(cs, clause, assumptions)
	} else {
	val (candidates, bodyNum) = availableStates(i)
	if (candidates.size == 1) {
	// the constraint has already been taken into account
	chosenStates(bodyNum) = candidates(0)._1
	findPreStates(i + 1, assumptions)
	} else {
	for ((state, simpStatePreds) <- candidates) {
	val newAssumptions =
	sf.reduce(conj(List(assumptions, simpStatePreds)))
	if (!newAssumptions.isFalse) {
	chosenStates(bodyNum) = state
	findPreStates(i + 1, newAssumptions)
	}
	}
	}
	}

	findPreStates(0, currentAssumptions)

	}