Open rasoolmaghareh opened 4 years ago
I added @joxanjaffar as a participant to receive updates via email.
My part of the implementation is finished. I created the PR #374.
The output of the half_interpolant.c
program in the basic folder is this:
Half Speculation set to:1 We reached here. Half Speculation set to:0 We reached here.
Hi @rasoolmaghareh: I am a little bit confused about how we can get the benefit of running in speculation mode, can you explain some more detail here? As I understand the execution of the two subtrees in the image I attached is the same right?
#include <klee/klee.h>
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
if (x < 0){
tracerx_half_speculation(0);
} else {
tracerx_half_speculation(1);
}
printf("We reached here.\n");
}
Original program:
#include <klee/klee.h>
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
printf("We reached here.\n");
}
Hi @rasoolmaghareh @xuanlinhha I ran speculation safety with custom on master branch (I am aware about the new timeout option is not implemented yet) on 9 programs with one run at a time style and we have good results as compared to KLEE and CBMC, but slower than Del-TX. Ofcoure we want to have better that Del-TX, but just wanted to cross check that whether our code is aligned with the decided metrics or not. Because I remember that in safety also we modified some checks.
OR should I run the programs with "maste_speculation_safety_fix" branch. Please do let me know asap. So, that i can reran and we can verify. Also, I feel my last night run will not be wasted because we can observe that out modification in code has some improvements.
I have checked the code as well as the log of master branch where I can see that, the current code is up to date and the changes from "maste_speculation_safety_fix" has been merged. It shows that for RERS and psyco series programs we have an overhead as compared to Del-TX.
We decided to follow @sanghu1790 suggestion for this branch. I am renaming it to Half-Speculation timeout. @sanghu1790 will take this over.
Considering our discussion yesterday. The following steps need to be implemented:
@rasoolmaghareh should implement:
halfSpeculation
. This variable is used by TracerX to determine at what point it should make a node speculation node.@xuanlinhha and @sanghu1790 should implement these steps:
1- Reading the value of variable
halfSpeculation
fromMu
(if exists). If it is1
, then the node should be set as a speculation node.2- In picking the next node, if for two siblings one is
normal
node and one isspeculation
node, thespeculation
node should be picked first.3- We need to check half-speculation with both cases of having the
linearity-bound
and not having thelinearity-bound
. We need to see which one is performing better.4- Half-speculation fails in two cases:
error
.