ensuring(rec <= ...) -- big verification time variation #214
Comments
|
Sorry for the delayed reponse. Can you send me the source file Scheduler.scala ? |
|
File attached. Scheduler.txt Now I have the following error: :) |
|
At line 396, the code uses 'rec' in the body of the function. Instrumentation variables |
|
Btw, if for some reason you need to count the number of recursions in the implementation, you have to maintain a counter say |
|
What I would like to prove is: def testEvolutionSimpleProofRec(c: Core, e:Task): Core = {
require(isUnique(c.tasks) && c.tasks.contains(e) && !c.current.isDefined && find(c.tasks,e).isDefined && !c.tasks.isEmpty);
val c2 = doubleTimer(c,e) // see doubleTimer def to know why we don't use timer directly
if(timer(c).current == Some(e)) {
c
} else if (find(doubleTimer(c,e).tasks, e).get == find(c.tasks, e).get - 1) {
doubleTimer(c,e)
} else { // otherwise recursive call
testEvolutionSimpleProofRec(c2, e);
}
} ensuring(res => (rec <= maxSumBeforeSorted(c.tasks, e) + ?));But for some reason Leon was not able to prove it. So I added a "if rec <= max else error" and it seemed to work, but really this is not necessary (in fact I would prefer not to do it) :) I tried to rerun leon with the function above (i.e., without the rec <= condition), but now I have this error :) |
|
Here is a higher level view of what I try to prove, if it might help: I have two values: a and b. doubleTimer either increments a if a < max, or decrements b, or changes the state to the final state. I try to prove that this function finishes (it does because a cannot grow unbounded, so we will eventually be in the final state or decrease b): Thanks :) |
|
Here is a minimal example that corresponds to the logic of what I want to prove (but for some reason I have a compile error due to rec? Am I missing something?) import leon.collection._
import leon.lang._
import scala.Any
import leon.annotation._
import leon.proof._
import leon.instrumentation._
import leon.invariant._
import leon.util.Random
object Scheduler {
case class Core(a:BigInt, b:BigInt, max:BigInt) {
}
def doubleTimer(c:Core):Core = {
if(c.a < c.max) {
Core(c.a + 1, c.b, c.max)
} else {
Core(0, c.b - 1, c.max)
}
}
def rec(c:Core):Core = {
val c2 = doubleTimer(c);
if(c2.b == c.b - 1) {
c
} else {
rec(c);
}
} ensuring(res => (rec <= c.max));
} |
|
The minimal example is much better for me to debug. In your example, there is a function called |
|
As the counter-example indicates: c.a could be greater than c.max and hence the function may not terminate |
|
There is one subtle issue here. The above function is non-terminating since you are making the recursive call with the same argument. Did you mean rec(c2) ? In any case, you need to make sure all functions are terminating before proving properties with leon. This is also true for rec. But, unfortunately, for various reasons, termination is not checked by "rec" function itself |
|
Indeed :) With this function it works :) def recF(c:Core):Core = {
val c2 = doubleTimer(c);
if(c2.b == c.b - 1) {
c
} else {
recF(c);
}
} ensuring(res => ((c.max < 0) || (rec <= c.max)));So I guess it should work too for my "real" example. So far I still have an error, but it seems unrelated to the "recursive checking": Scheduler.txt |
|
Actually, it is somewhat unsound in your example because your example does not terminate on all inputs. As I had mentioned, you must make sure that all functions terminate. Run termination phase as well, everytime you check properties with Leon. |
|
I will look into the crash |
|
I have fixed the crash in your example. Can you try it again. But, remember that you need to check termination of all functions as well. |
|
Yes, the functions I check in the real example terminate :) (Actually in the small example the function should have too... I wanted to do the recursion with c2 as parameter, not c... well...) Anyways, now I get the following error, I am missing something? (Using e516634) |
|
I don't get this error. Did you compile the build ? Also, can you run without --functions option. Also send me the Scheduler.scala file you are using. |
|
The file I use is: https://github.com/epfl-lara/leon/files/383971/Scheduler.txt I did Also I run the code on an 8-core machine (I don't know what you use, I might have more concurrency issues?). Thanks :) |
|
Sorry for the delayed response. I investigated this error. It is due to the use of "rec" in the body of function |
|
Were you able to fix this ? I am back at EPFL. If you want we can meet in person. |
|
Without rec it compiles now :) The only issue I currently have is that Leon is not able to prove functions that it used to be able to prove (e.g., insertTask in https://github.com/epfl-lara/leon/files/383971/Scheduler.txt ), but I've not investigated the issue fully. I've got a deadline on the 15th, but I'll get back to proofs seriously after that! ;) Thanks :) |
|
Okay. Just one comment. |
Using 624e5a7
I am trying to prove that a function terminates by ensuring that "rec <= someValue". The time to check the postcondition varies a lot : checking the exact same file, it might take between 30s and 700s to validate the property (I might also have had some runs in which the validator never ends).
I know that this is a pretty vague issue, but if you have any idea on how to report more precise data, I can try it :)
Scheduler.txt
Some timings also surprise me:
On that code, the body assertion is always much faster than checking the postcondition, while the postcondition seems easier to check (it derives directly from the ifs). Any insight on why this is the case?
All tests are done on a fairly recent desktop machine with 8 cores.
The text was updated successfully, but these errors were encountered: