Speculation -spec-type=coverage not working on one example.

[rasoolmaghareh]

@sanghu1790, I moved your message to a new issue. I think the two issues in speculation are different.

Hi Rasool and Linh,

I experimented the program for the speculation slowness issue.
I ran "Mpals6-B2-cil.c" program which is big in size, but to see the difference
I found it suitable. Later we can reduce the size or take some other small program.

After my current investigation and recalling previous conversations, the issue of slowness
is due to running a program with and without providing "Spec_Avoid" files (these are dependent
files after prepossessing).
I ran the programs with and without Spec_Avoid file on following commits:

1. master-0df7858a09741d0e19809dcc1a19fffd1179e445
2. spec_custom_dyn-cfeb033c8912a8ce6ba84ed2b3f1117915fe40d3(most-recent)
3. spec_custom_dyn-ab4f9fb8cc0869e99a507b2512c97a505266b255(two-commits-back)

A. For the experiment with Spec_Avoid files on 1, 2, and 3, all finished in
35 sec approx. And also I see their stats are also same. But, some numbers
in spec.txt files of all these three results are little changed, that I think
we can check, why it had happened.

B. For the experiment without Spec_Avoid files on 1 and 3 above are very slow (THE PROBLEM WE ARE DEALING),
whereas for 2, it is very fast and finished in 34 sec approx, just like happened in A above.
Also, here the info stats and spec.txt files are very different.

From the above investigation, I have observed that "Removing Independence checks" and without Spec_Avoid files
works very faster as compared to others. My question is why providing dependency files or not so much matter
in performance? If we provide dependency files then the checking time should be more so it should be more expensive,
but if we dont provide any such files so still it should be faster. At least the master branch should be align with
spec_custom_dyn (most recent) branch. But, I remember this during the preparation of master branch we took the decision
to not to "Removing Independence checks" from speculation sub-tree. Now, we can discuss after looking into consequences.

Still, @linh, please check why our metrics stats of info and spec.txt files of these are different. Is there any mistake or
every thing is fine.

@rasool, Just to tell you, if you remember I encountored this issues because we were trying to run spec, with different number of
Spec_Avoid files (like all files, no files, only one file, deleting one file) etc. And our observation was different performance on different runs.
Then we discussed and agreed that, if we dont provide any files still it should work fine, but this is not the case now in master branch.

All, files and results are in zip folder, have a look.
Speculation-fix.zip

I ran with these commands:

Run master branch
/home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -spec-dependency=/home/sanghu/Desktop/Speculation-fix -spec-strategy=custom -spec-type=coverage ${BENCHMARK}.bc

Run spec_custom_dyn branch
/home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -speculation ${BENCHMARK}.bc

Thanks,
sanghu

[xuanlinhha]

I ran master-0df7858a09741d0e19809dcc1a19fffd1179e445 without spec avoid file but it not finished on my machine

[xuanlinhha]

@sanghu: on spec_custom_dyn how do you specify the folder containing spec avoid files ?

[sanghu1790]

@xuanlinhha To run master branch in speculation mode I have used this command:

/home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -spec-dependency=/home/sanghu/Desktop/Speculation-fix -spec-strategy=custom -spec-type=coverage ${BENCHMARK}.bc

Here, -spec-dependency=/home/sanghu/Desktop/Speculation-fix is the path to put Spec_Avoid files. SpecAvoid files should be inside Speculation-fix.

Please note that for 'spec_custom_dyn' we dont provide '-spec-dependency' command, in that case the current directory will be the place where Spec_Avoid files should be kept.

[xuanlinhha]

Hi @sanghu1790 I tried to reproduce your result but for this branch spec_custom_dyn-ab4f9fb8 with speculation files, the result I received is like this:

KLEE: KLEE: WATCHDOG: watching 10164

KLEE: output directory is "/home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil"
Using Z3 solver backend
tcmalloc: large alloc 1452982272 bytes == 0x1040d8000 @ 
tcmalloc: large alloc 1452982272 bytes == 0x109afe000 @ 
tcmalloc: large alloc 1452982272 bytes == 0x108fcc000 @ 
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT

KLEE: ctrl-c detected, requesting interpreter to halt.
tcmalloc: large alloc 2147491840 bytes == 0x262388000 @ 
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via gdb

Could not attach to process.  If your uid matches the uid of the target
process, check the setting of /proc/sys/kernel/yama/ptrace_scope, or try
again as the root user.  For more details, see /etc/sysctl.d/10-ptrace.conf
ptrace: Operation not permitted.
No symbol table is loaded.  Use the "file" command.
The program is not being run.
KLEE: WARNING: KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)

[sanghu1790]

@xuanlinhha Can you please cross verify the command options:
Run spec_custom_dyn branch
"/home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -speculation ${BENCHMARK}.bc" Keep your and mine parameter same.

Secondly also cross verify the Spec_Avoid files placed at the current directory where your "c" program and make script are running. I believe the problem is just run issue.

[xuanlinhha]

/home/xuanlinhha/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -speculation -output-dir=/home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil /home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil.bc

[sanghu1790]

Yes. This is correct command option. Can you run and check? The program should finished in approx 35 sec.

[xuanlinhha]

no, it is timeouts on my machine, attached is the result:
Mpals6-B2-cil_spec_custom_dyn-ab4f9fb8-with-spec.zip

[sanghu1790]

Can you check if Spec_Avoid files are stored here "/home/xuanlinhha/TracerX/run-test/output/" on your machine.
This is my results, please cross verify:
Mpals6-B2-cil-5--spec_custom_dyn-ab4f9fb8cc0869e99a507b2512c97a505266b255(two-commits-back).zip
Still I suspect you are not providing the specavoid files properly.

[sanghu1790]

This is yours @xuanlinhha
Total Independence Yes: 16815
Total Independence No: 0
Total Dynamic Yes: 0
Total Dynamic No: 0
Total Independence No, Dynamic Yes & Success: 0
Total Independence No, Dynamic Yes & Fail: 0
Total speculation failures because of New BB: 0
Total speculation failures because of New BB with no interpolation: 0
Total speculation failures because of Revisted: 0
Total speculation failures because of Revisted with no interpolation: 0
Total speculation failures because of Bug Hit: 0
Total speculation fail time: 0
Frequency of failures because New BB with no interpolation:
Frequency of failures because Revisted with no interpolation:

This is mine results:
Total Independence Yes: 0
Total Independence No: 2736
Total Dynamic Yes: 1417
Total Dynamic No: 1319
Total Independence No, Dynamic Yes & Success: 1171
Total Independence No, Dynamic Yes & Fail: 246
Total speculation failures because of New BB: 239
Total speculation failures because of New BB with no interpolation: 239
Total speculation failures because of Revisted: 7
Total speculation failures because of Revisted with no interpolation: 5
Total speculation failures because of Bug Hit: 0
Total speculation fail time: 0.682169
Frequency of failures because New BB with no interpolation:
54249128: 3
54251592: 10
54251816: 63
54253496: 10
54255960: 9
54256184: 7
54257864: 9
54260328: 8
54260552: 6
54262232: 9
54457760: 12
55198616: 7
55198840: 5
55200520: 11
55202984: 6
55203208: 7
55204888: 6
55207352: 5
55207576: 8
55209256: 5
55211720: 4
55211944: 9
55213624: 4
55232504: 3
55232728: 10
55368840: 1
55381856: 2
Frequency of failures because Revisited with no interpolation:
54405400: 3
55383584: 2

It shows that your run doesn't read spec avoid files.

[xuanlinhha]

// load avoid BB
  bbOrderToSpecAvoid = readBBOrderToSpecAvoid("/home/xuanlinhha/TracerX/run-test/Speculation-fix/Mpals6-B2-SpecAvoid");
  llvm::errs() << "bbOrderToSpecAvoid size = " << bbOrderToSpecAvoid.size() << "\n";

I fixed the path into source code, and it prints:
bbOrderToSpecAvoid size = 1
is that correct?

[xuanlinhha]

And I am working on this commit: ab4f9fb8cc0869e9
Do you see it is strange here @sanghu1790 ?

name=SpecAvoid_149.txt
name=SpecAvoid_155.txt
...
name=SpecAvoid_20.txt
name=SpecAvoid_167.txt

bbOrderToSpecAvoid size = 1

it can see all the files in the folder but just only have 1 BB

[sanghu1790]

@xuanlinhha First of all tell me this new run was faster? Did it finished in 35 sec.

[xuanlinhha]

no @sanghu1790, it does not run faster at all, it was a timeout

[sanghu1790]

I just ran the same program ans it finished in 36 sec.
I ran on this commit:

commit ab4f9fb
Author: xuanlinhha xuanlinhha@gmail.com
Date: Wed Sep 25 13:41:00 2019 +0800

Temporary fix for getting depending variables' name

---

Using this command: /home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -speculation ${BENCHMARK}.bc

Result is here:
Linh-email.zip

Make sure that all spec avoid files are in same directory where .bc file exist.

[xuanlinhha]

Hi @sanghu1790,
With speculation avoid files, we have 3 versions:

1. master-0df7858
2. spec_custom_dyn-cfeb033c
3. spec_custom_dyn-ab4f9fb8

1 vs 2: Cannot compare because in 2 we don't check dependency
1 vs 3: The numbers in spec.txt are different because in 3 we count independenceYes/independenceNo and dynamicYes/dynamicNo in speculationFork. If we delete the increasing in speculationFork, the numbers will be the same. You can check again this

[sanghu1790]

Hi @xuanlinhha
Point A: 1 vs 2: Cannot compare because in 2 we don't check dependency
Answer: I agree.

Point B: 1 vs 3: The numbers in spec.txt are different because in 3 we count independenceYes/independenceNo and dynamicYes/dynamicNo in speculationFork. If we delete the increasing in speculationFork, the numbers will be the same. You can check again this
Answer: I am fine with this mismatch in the counting, and we can rely on the new counting on master branch, since now we are using MAP (I remember). Thanks for above justifications.

Now @xuanlinhha , can you also try above without Spec_Avoid files? We need to check, why 1 and 3 took more than 600 sec and 2 finished in 36 sec (on machine). Is it the only difference of disabling "Independence Checks" in "speculationFork" or something else? If it is the case then why in master branch we dont follow disabling "Independence Checks" in "speculationFork"?

[xuanlinhha]

@sanghu1790 When running without spec avoid files, 1-3 is corresponded to -spec-strategy=custom -spec-type=coverage and 2- is -spec-strategy=custom -spec-type=safety in current master branch.
But when I run with -spec-strategy=custom -spec-type=coverage, I see there are bug, so I need to check the cause why

[xuanlinhha]

slow-running.zip
@sanghu1790 the problem of slow running now become this:
-spec-strategy=custom -spec-type=coverage is slower than -spec-strategy=custom -spec-type=safety
The difference between 2 versions is that described in this matrix:

When running without speculation avoid file, the independency check always returns True

[sanghu1790]

@xuanlinhha Thanks linh.
You mean all time Independence check will be YES.
So, then body of this condition will satisfy.

if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
            // open speculation & assume success
            independenceYes++;
            //          StatsTracker::increaseEle(curBB, 0, true);
            //          StatsTracker::increaseEle(curBB, 2, false);
            return StatePair(&current, 0);
          }

But, I dont see any other stuff above which will take heavy time.
What went wrong after this?

[xuanlinhha]

Yes, this is -spec-strategy=custom -spec-type=coverage

Total Independence Yes: 47673
Total Independence No: 0
Total Dynamic Yes: 0
Total Dynamic No: 0

Yes, this is -spec-strategy=custom -spec-type=safety

Total Independence Yes: 0
Total Independence No: 0
Total Dynamic Yes: 193
Total Dynamic No: 1
Total Independence No, Dynamic Yes & Success: 131
Total Independence No, Dynamic Yes & Fail: 62

Why it runs slow, this is I also don't know

[sanghu1790]

@xuanlinhha
As I can see if we have independece check YES then we just assume the spec success happened, and not marking.

Can we try running with marking for this special case and let see what happens?
Add this txTree->markPathCondition(current, unsatCore); and check?

Copy this below code and let us see what happens here.

if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
            // open speculation & assume success
            independenceYes++;
            //          StatsTracker::increaseEle(curBB, 0, true);
            //          StatsTracker::increaseEle(curBB, 2, false);
          txTree->markPathCondition(current, unsatCore);
            return StatePair(&current, 0);
          }

[xuanlinhha]

it also gives a timeout @sanghu1790
If we do in that way, equivalent to all speculations are fail.

[sanghu1790]

Hi @xuanlinhha
As we discussed I ran TIMID and CUSTOM on master branch.

1. TIMID (WITH SPEC AVOID FILES)= Approx. 200 sec and timeout
2. TIMID (WITHOUT SPEC AVOID FILES)= Approx. 200 sec and timeout
3. CUSTOM (WITH SPEC AVOID FILES)= 27 sec and finished
4. CUSTOM (WITHOUT SPEC AVOID FILES)= Approx. 200 sec and timeout
   TIMID-CUSTOM-MASTER-RESULT.zip
   You can check their spec.txt files in this zip file.

[sanghu1790]

@xuanlinhha I ran on fix_skip_void_type after fixed issue, still the same results.

1. TIMID (WITH SPEC AVOID FILES)= Approx. 200 sec and timeout
2. TIMID (WITHOUT SPEC AVOID FILES)= Approx. 200 sec and timeout

I think if we are able to get to know that why without specavoid files TIMID isn't working, then automatically the CUSTOM issue will also get fixed.

But interesting fact is below:

1. Below is spec stats for TIMID (WITH SPEC AVOID FILES)

Total Independence Yes: 0
Total Independence No: 405
StatsTracker Total: 0
StatsTracker Fail: 405
StatsTracker Success: 0
Total speculation failures because of New BB: 0
Total speculation failures because of New BB with no interpolation: 0
Total speculation failures because of Revisted: 0
Total speculation failures because of Revisted with no interpolation: 0
Total speculation failures because of Bug Hit: 0
Total speculation fail time: 0
Frequency of failures because New BB with no interpolation:
Frequency of failures because Revisted with no interpolation:

2. Below is spec stats for TIMID (WITHOUT SPEC AVOID FILES)

Total Independence Yes: 39098
Total Independence No: 0
StatsTracker Total: 39098
StatsTracker Fail: 0
StatsTracker Success: 39098
Total speculation failures because of New BB: 0
Total speculation failures because of New BB with no interpolation: 0
Total speculation failures because of Revisted: 0
Total speculation failures because of Revisted with no interpolation: 0
Total speculation failures because of Bug Hit: 0
Total speculation fail time: 0
Frequency of failures because New BB with no interpolation:
Frequency of failures because Revisted with no interpolation:

Both 1 and 2 above tool huge time of 200 sec. It should be rapidly work.
Now, I think the problem is coming from somewhere else.
I suspect the check with "NEW BB". Cam we turnoff this check during the coverage mode? I want to see the difference. Make a new commit with commented code for the check of NEW BB. Later we will delete that commit if it doesn't work.

[xuanlinhha]

We don't need to commit with just a comment @sanghu1790 , I commented and tested on my local machine, but it is still slow

[xuanlinhha]

@sanghu1790 the problem now is becoming like this:
Untitled spreadsheet - Sheet1 (3).pdf

I remove New BB checking, run with -spec-strategy=custom -spec-type=coverage, and change value returned from Independence checking. Because we run without spec avoid files, so if Independence checking always returns FALSE, it is equivalent with -spec-strategy=custom -spec-type=safety

The strange statistics is like this:

|=> First Case | completed paths = 374 | subsumed paths = 365 | BCov(%) = 77.85
|=> Second Case | completed paths = 4037 | subsumed paths = 4006 | BCov(%) = 30.87

info-First Case.txt
info-Second Case.txt

[sanghu1790]

Hi @xuanlinhha ,
Yeah I see your point. This is strange stats. As per your defined cases, First-case has all time "dynamic checks" and it will explore speculation sub-stree, so it's paths and coverage must be more that normal. In second case, we assume all time "Independence checks" are YES, so we assume all time spec successes. Here, in second case we dont create the speculation sub-stree and we see the paths are more and coverage is less than the first case.

What I am thinking now is to put "dynamic check" inside "Independence check YES" to check the situation what will happen. What I can estimate here is that, if this is true then we need to make below:

For coverage mode

1. With spec avoid files: Keep "Independence check", "dynamic check" , and "New BB check".
2. Without spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

Whats your opinion?

[rasoolmaghareh]

May I also confirm here that the current implementation with spec-avoid files is working fine with the following setting?

1- With spec avoid files: Keep "Independence check", "dynamic check", and "New BB check".

If so, I think I agree with @sanghu1790 for setting 2 when we don't have spec-avoid files.

[sanghu1790]

@rasoolmaghareh

1. Up to now setting 1 was working well as per my experience. But, when we will do actual experiments on all programs then, we can observe the real scenario.

2. One more point is that, if we will supply spec avoid files then they should be complete set (after pre-processing) OR dont supply any files, for the correct results. But, supply of partial spec avoid files (either supply one file or (n-1) where n is the total spec avoid files) is not recommended. The performance may hamper.

[rasoolmaghareh]

ok, for conclusion let's consider these two cases and confirm they are correct for coverage mode:

1- With complete set of spec avoid files: Keep "Independence check", "dynamic check" , and "New BB check".

2- Without any spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

[sanghu1790]

Yes I agree with this.

@xuanlinhha Whats your opinion?
Do you want to do more finding on "independence check YES" case?

@rasoolmaghareh honestly I and linh didn't got the real answer why "independence check YES" is taking huge time. My proposal was based on the several attempts we made to see the best results, and we found this case. Do you have any idea about the above case where "independence check YES" is so expensive?

[xuanlinhha]

@rasoolmaghareh:

2- Without any spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

=> In safety we don't have "New BB check"

@sanghu1790: I think if users run with coverage but not provide spec avoid files, we can print an error message and ask them to run with safety

[sanghu1790]

Hi @xuanlinhha
Rasool and I both are aware about point number 2 for coverage is with "New BB check" and safety is without "New BB check". Don't worry we all are on same page. Am I right @rasoolmaghareh .

Regarding the printing message, I agree @xuanlinhha but we need to facilitate the users to use without specavoid files too. Hence we require point 2 for that. But we can give warning message.

[rasoolmaghareh]

yes.

[xuanlinhha]

But if like this:

2- Without any spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

Cannot resolve the program of @sanghu1790

[sanghu1790]

@xuanlinhha

I am referring your comment #364 (comment)
and my comment #364 (comment),
I estimate that

2- Without any spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

will run faster based on your sample run.

But yeah before merging to master branch we should run couple of programs.

But, overall my view would be to run coverage with mandatory spec avoid files. We will take final decision based on experiments.

[xuanlinhha]

I have checked on my side, and no non-speculation states are deleted when backjump
But one thing I noticed is that all the interpolants inside the speculation subtree only contain the counter variable i2=1 but the from non-speculation nodes contain many information being marked.
Maybe the interpolant inside spec-tree make more subsumption checks success and we run faster

[rasoolmaghareh]

Can you please share the generated interpolants in both speculation tree and outside speculation tree here?

[xuanlinhha]

The second file is big, so I zipped it:
intepolant-in-spec-output.txt

interpolant-out-spec-output.txt.zip

You see the marked variables are global ones.
All interpolations outside spec-tree have symbolically-addressed store = []

[rasoolmaghareh]

I have checked these files and the better interpolants are due to the point that speculation is successful. So no errors in this part. May I ask if you @sanghu1790 @xuanlinhha see any issues in the speculations? If no issues I think the programs are fine.

In order to recap, @sanghu1790 Can you please advice on the matrix what are the current issues that we have to look at?

[rasoolmaghareh]

@sanghu1790 @xuanlinhha Can you please give an update here?

[sanghu1790]

Hi @rasoolmaghareh @xuanlinhha
I read our entire conversation, and recalled my views. I feel we did everything to verify to solve the issues. I consolidate my opinion as below:

1. Observations on command settings.
   =======================================================================
   A: -spec-strategy=custom -spec-type=safety
   Without any spec avoid files: Keep "dynamic check" only
   =======================================================================

=======================================================================
B: -spec-strategy=custom -spec-type=coverage

Here, we may have two sub-options -spec-Independence=YES or NO

B1- -spec-strategy=custom -spec-type=coverage -spec-Independence=YES
With complete set of spec avoid files: Keep "Independence check", "dynamic check" , and "New BB check". ()

NOTE: It should be complete set (after pre-processing). Supply of partial spec avoid files (either supply one file or (n-1) where n is the total spec avoid files) is not recommended it may hamper performance.

B2- -spec-strategy=custom -spec-type=coverage -spec-Independence=NO
Without any spec avoid files: Keep "dynamic check", and "New BB check"

=======================================================================

2. @xuanlinhha I am aware about that B2 is still running slow for the sample program we have chosen. It happened to be a bad sample in this case, and it helped us to understand that we must have two options B1 and B2 to have good results. So, dont worry for this, we will experiment with our benchmark to observe the results.

3. @rasoolmaghareh @xuanlinhha Also, I feel we should remove TIMID and AGGRESSIVE options, just keep CUSTOM. I feel they dont add anything in our results. Please think of it. But, yeah we must have one mode of RV implementation to compare as our baseline.

4. @rasoolmaghareh @xuanlinhha Apart from all these observations I have one suggestion to add one command line option for both safety and coverage modes where we will give the choice to user to turn-on/off the checks inside "speculationFork". As per my past experience with spec experiments I have seen several such situations, and the results were good in both cases.

Please share your views on above, so that we can close this thread.

Thanks,
Sanghu

[xuanlinhha]

@sanghu1790 So do you want 1 more option -spec-Independence to decide whether there is dependency check in branchFork or speculationFork or both?

[sanghu1790]

Hi @xuanlinhha ,
Yeah for B1 : ENABLE ON BOTH and B2: DISABLE ON BOTH.

Separately,
Regarding point number 4, My suggestion was for safety as well as overage, where we must give the choice to the users, of ENABLING/DISABLING all checks (Independence check, custom check, NEW BB check) in speculationFork. If this command is Enabled then, all checks should be enabled in branchFork but should be disabled in speculationFork.
Default should be the disable of this command, i.e. All checks are as in branchFork and speculationFork as per our matrix.

[xuanlinhha]

• For this option: -spec-Independence:
  If set True: enable independence checking in both fork functions
  If set False: disable independence checking in both fork functions

• For one option in speculationFork: There is no NEW BB check in this function, it only has independence and dynamic checkings. This option does not have any effects to branchFork? and what is the behavior do you want?

[sanghu1790]

For this option: -spec-Independence:
If set True: enable independence checking in both fork functions
If set False: disable independence checking in both fork functions
Answer: You are correct

For one option in speculationFork: There is no NEW BB check in this function, it only has independence and dynamic checkings. This option does not have any effects to branchFork? and what is the behavior do you want?
Answer: In safety "NEW BB" will be absent, but it should be in coverage right? What are you saying, NEW BB is present in branchFork and absent in speculationFork? Is it?
After enabling this command, I wanted to disable all checks from speculationFork and keep remain in branchFork.

[xuanlinhha]

What I mean is that in speculationFork, there are also 2 checkings: independence and dynamic
NEW BB is present in branchFork and absent in speculationFork? Is it? => currently, NEW BB checking is done in COVERAGE no matter it is in branchFork or speculationFork

[sanghu1790]

Ohh I see, NEW BB check doesn't belong to speculationFork. I am sorry for this. Yeah you are correct, we please ignore that part where I said on NEW BB check, and consider other checks.

[xuanlinhha]

@sanghu1790 I want to apply the new option to Coverage mode only because currently I see in Safety mode we don't have any independence check at all and I want to keep this setting for Safety mode. Do you agree?

[rasoolmaghareh]

I agree with the conversation. Let's apply these changes to coverage and close this issue.

[xuanlinhha]

I have added one more option -spec-independence in branch dependence-check-option, if it is disabled, there is no independence in both fork functions and it behaves like safety mode.
Can you see if there is any error?

[sanghu1790]

Thanks @xuanlinhha Now I will work on that.

[rasoolmaghareh]

@sanghu1790 Can you please check this issue and in case the code is correct we close this issue.

[sanghu1790]

Hi @xuanlinhha ,
I was checking the code of "master" branch and "dependence-check-option" branch. It seems to be that we have not merged this branch yet into master. Today, Rasool and I decided that for safety mode as well we must provide an option for providing SpecAvoid files, just like you did for Coverage mode. Please note that the only difference with safety and coverage will be the extra check of "NewBB" for AGGRESSIVE and CUSTOM. You make sure that for safety and coverage modes we will have the option of either providing SpecAvoid files or not. Can you please do this as an urgency basis? I require this asap.

[xuanlinhha]

Hi @sanghu1790
This option spec-dependency is available no matter which mode are running

if (INTERPOLATION_ENABLED && SpecTypeToUse != NO_SPEC) {
    independenceYes = 0;
    independenceNo = 0;
    dynamicYes = 0;
    dynamicNo = 0;
    specFail = 0;
    totalSpecFailTime = 0.0;
    for (std::map<llvm::Instruction *, unsigned int>::iterator
             it = specSnap.begin(),
             ie = specSnap.end();
         it != ie; ++it) {
      it->second = 0;
    }
    // load avoid BB
    bbOrderToSpecAvoid = readBBOrderToSpecAvoid(DependencyFolder);
    visitedBlocks = readVisitedBB(DependencyFolder + "/InitialVisitedBB.txt");
  }

If you provide InitialVisitedBB.txt in that dependency folder, it will be used in checking new BB, but the checking new BB is done with Coverage mode