<div dir="ltr">Hi Pavel<div><br></div><div>Thank you very much for your reply! It is very helpful!</div><div><br></div><div>Sincerely,</div><div>Tuo Li</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Oct 3, 2023 at 3:58 PM Павел <<a href="mailto:andrianov@ispras.ru">andrianov@ispras.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear Tuo Li,<br>
<br>
Thank you for the interest in the Klever framework.<br>
<br>
CPALockator is enabled automatically, when you are verifying <br>
"concurrency safety" property. So, to enable it you just need to modify <br>
job.json and add "concurrency safety" into "requirement specifications".<br>
<br>
All available requirement specifications are described in <br>
specifications/Linux.json, section "requirements specifications".<br>
<br>
Best regards,<br>
Pavel<br>
<br>
03.10.2023 08:09, Tuo Li пишет:<br>
> Hi,<br>
><br>
> I have tried to use Klever to detect data races in Linux 6.2 with <br>
> CPALockator.<br>
> But I can not find how to enable CPALockator.<br>
><br>
> I first deployed Klever with the default configure <br>
> file klever/deploys/conf/klever.json.<br>
> I found that CPALockator is enabled in klever.json.<br>
><br>
> And Then I ran the following command to prepare the build base as <br>
> introduced in the tutorial.<br>
> clade -w ~/build-base-linux-6.2-x86_64-allmodconfig -p <br>
> klever_linux_kernel --cif $KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/cif <br>
> make -j8 modules<br>
><br>
> After the compiling was done, I performed the verification as <br>
> described in the tutorial.<br>
> However, I do not know how to modify job.json and tasks.json to enable <br>
> CPALockator.<br>
><br>
> Any feedback will be appreciated!<br>
><br>
> Sincerely,<br>
> Tuo Li<br>
><br>
> _______________________________________________<br>
> ldv-project mailing list<br>
> <a href="mailto:ldv-project@linuxtesting.org" target="_blank">ldv-project@linuxtesting.org</a><br>
> <a href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project" rel="noreferrer" target="_blank">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a><br>
</blockquote></div>