[ldv-project] Detecting data races in Linux 6.2 with CPALockator

[Павел]

Dear Tuo Li,

Thank you for the interest in the Klever framework.

CPALockator is enabled automatically, when you are verifying 
"concurrency safety" property. So, to enable it you just need to modify 
job.json and add "concurrency safety" into "requirement specifications".

All available requirement specifications are described in 
specifications/Linux.json, section "requirements specifications".

Best regards,
Pavel

03.10.2023 08:09, Tuo Li пишет:
> Hi,
>
> I have tried to use Klever to detect data races in Linux 6.2 with 
> CPALockator.
> But I can not find how to enable CPALockator.
>
> I first deployed Klever with the default configure 
> file klever/deploys/conf/klever.json.
> I found that CPALockator is enabled in klever.json.
>
> And Then I ran the following command to prepare the build base as 
> introduced in the tutorial.
> clade -w ~/build-base-linux-6.2-x86_64-allmodconfig -p 
> klever_linux_kernel --cif $KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/cif 
> make -j8 modules
>
> After the compiling was done, I performed the verification as 
> described in the tutorial.
> However, I do not know how to modify job.json and tasks.json to enable 
> CPALockator.
>
> Any feedback will be appreciated!
>
> Sincerely,
> Tuo Li
>
> _______________________________________________
> ldv-project mailing list
> ldv-project at linuxtesting.org
> http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project