burcuku / check-lin

Checking Linearizability using Hitting Families
1 stars 1 forks source link

How to generate the .json files? #1

Open alaukiknpant opened 4 years ago

alaukiknpant commented 4 years ago

How do we generate the .json files used for checking the linearizability of concurrent data structures? Will this code base work if we want to analyse more complex concurrent Scala code?

alaukiknpant commented 4 years ago

@burcuku

burcuku commented 4 years ago

Hi @alaukiknpant, I generated the .json files (i.e., the histories to be analyzed) using Violat. You can follow the steps in its repo to generate history files for the java concurrent data structures. The parameters for test harnesses to generate execution histories are specified in the folder "resources/specs/java/util/concurrent".