#Violat

[jayrathi5]

978-3-030-25543-5_30 (1).pdf

This tool also work in similar fashion but I think Violat will take less time because we are generating Schemas(Concurrent Scenario) sequentially before running them actually then just comparing.I am not sure can you tell me what's the difference between them.

[ndkoval]

@jayrathi5, could you please clarify what exactly should take less time and what the difference you see?

[jayrathi5]

@ndkoval The violat tool will take less time in generating scenarios as in lincheck with stress testing we randomly generate a scenario and run it but in violat first it is preparing scenarios and then executing this scenarios multiple time to get various output.

[eupp]

Hi @jayrathi5 !

I've tried to skim through the article. From what I understood, Violat works as follows:

1. It generated a set of small test programs for a given data structure (we call them scenarios in Lincheck).
2. For each scenario it generated a set of possible outcomes allowed by data structure specification.
3. It then runs the scenario via stress-testing and checks that each outcome is in the set of allowed outcomes from step (2).

Lincheck basically works in the same vein, with the only difference that steps (2) and (3) are performed in different order:
we first execute scenario and then check that the outcome is allowed. Thus we do not try to enumerate all possible allowed outcomes, but rather do it lazily, trying to verify only the observed outcomes. Since Lincheck caches the set of allowed outcomes between invocations, no unnecessary re-computations are performed.

Thus I don't see a significant conceptual difference between these two approaches.
If I misunderstood something, feel free to respond.

[jayrathi5]

Hi @jayrathi5 !

I've tried to skim through the article. From what I understood, Violat works as follows:

1. It generated a set of small test programs for a given data structure (we call them scenarios in Lincheck).
2. For each scenario it generated a set of possible outcomes allowed by data structure specification.
3. It then runs the scenario via stress-testing and checks that each outcome is in the set of allowed outcomes from step (2).

Lincheck basically works in the same vein, with the only difference that steps (2) and (3) are performed in different order: we first execute scenario and then check that the outcome is allowed. Thus we do not try to enumerate all possible allowed outcomes, but rather do it lazily, trying to verify only the observed outcomes. Since Lincheck caches the set of allowed outcomes between invocations, no unnecessary re-computations are performed.

Thus I don't see a significant conceptual difference between these two approaches. If I misunderstood something, feel free to respond.

What I understood from the linCheck paper is that for a particular scenario it will generate a LTS(Labelled Transistion System) (by executing that interleaving sequentially) if we don't provide the specification .Please correct me if I am wrong.
Thanks for your reply now I understood the subtle difference between them.

[eupp]

particular scenario it will generate a LTS(Labelled Transistion System) (by executing that interleaving sequentially)

Lincheck will "generate" LTS in both cases: if you provide specification or not. But LTS is just an abstraction level over the data-structure.

The difference is that if you provide sequential specification class explicitly, then it will be used to check for outcome validity (linearizability). Otherwise, the data structure itself will be used to check outcome validity. So the Lincheck will execute the scenario concurrently, get some outcome, and then will try to validate it by trying to generate a sequential run of the same scenario leading to the same outcome.