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

[Tuo Li]

Hi Pavel

Thank you very much for your reply! It is very helpful!

Sincerely,
Tuo Li

On Tue, Oct 3, 2023 at 3:58 PM Павел <andrianov at ispras.ru> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20231003/fb08285a/attachment.html>