search

runtimeverification / rv-predict

Code for improved rv-predict and installer
BSD 3-Clause "New" or "Revised" License
2 stars 3 forks source link

sliced causality revisited #244

Open yilongli opened 9 years ago

yilongli commented 9 years ago

I personally like the idea of sliced causality a lot. And I consider our branch model to be an instance of the sliced causality that only captures the control-flow part. I understand that the static analysis in our old implementation is slow but I believe static analysis like this can be implemented quite efficient. Besides, we have better framework support than several years ago. Anyway, I believe we should explore the use of sliced causality again after we have a robust RV-Predict.

grosu commented 9 years ago

I agree! Static analysis may also help us a lot wrt minimizing instrumentation. The challenge is how to make it efficient.

Grigore

From: Yilong Li [notifications@github.com] Sent: Friday, December 26, 2014 12:43 PM To: runtimeverification/rv-predict Subject: [rv-predict] sliced causality revisited (#244)

I personally like the idea of sliced causality a lot. And I consider our branch model to be an instance of the sliced causality that only captures the control-flow part. I understand that the static analysis in our old implementation is slow but I believe static analysis like this can be implemented quite efficient. Besides, we have better framework support than several years ago. Anyway, I believe we should explore the use of sliced causality again after we have a robust RV-Predict.

— Reply to this email directly or view it on GitHubhttps://github.com/runtimeverification/rv-predict/issues/244.

yilongli commented 9 years ago

Grigore's comment copied from https://github.com/runtimeverification/rv-predict/issues/332#issuecomment-75749264:

1) I think we should first have a version of the tool without branches and without sliced causality, and hopefully that to be good enough that we can go public with it.

2) Then try to add branches only, like in the PLDI'14 paper, but to also take into account where the branch starts. It is a bit ridiculous to consider that a branch depends on ALL the previous reads in a thread, when in fact it only depends on the reads happening while the condition is evaluated. Once implemented, then evaluate its runtime overhead and overall effectiveness, to see whether it is worth introducing it as an option.

3) Go for sliced causality, which in fact means to start developing our own static analysis infrastructure in RV. Yes, because I think we should use the same in RV-Monitor to reduce the instrumentation overhead, and perhaps in other tools we have, too.