Half-Speculation Timeout Exploration

[rasoolmaghareh]

Considering our discussion yesterday. The following steps need to be implemented:

@rasoolmaghareh should implement:

1. A function that receives a value 0,1 and sets it in a special variable 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 from Mu (if exists). If it is 1, 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 is speculation node, the speculation node should be picked first.

3- We need to check half-speculation with both cases of having the linearity-bound and not having the linearity-bound. We need to see which one is performing better.

4- Half-speculation fails in two cases:

• A node hits error.
• We hit 20 or 30 minute timeout.

[rasoolmaghareh]

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.

[xuanlinhha]

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");
} 

[sanghu1790]

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.

[sanghu1790]

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.

[rasoolmaghareh]

We decided to follow @sanghu1790 suggestion for this branch. I am renaming it to Half-Speculation timeout. @sanghu1790 will take this over.