<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Hi Ilia!<br>
<br>
On 06.11.2018 18:50, Ilja Zakharov wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAAGy8gnKdT4rmPwKnyXJzpYG1ZTYwiRr-MSSFwxiW5m99ZABPA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<div dir="ltr">
<div>Dear Ahmet,</div>
<div><br>
As Evgeny Novikov promised (he is giving a talk at a
conference), below is the short guide for deploying and
running the Klever 2.0 software verification framework.<br>
</div>
<div><br>
</div>
<div>1. Choose your favorite Ubuntu/Debian image. The
instruction below is prepared for Ubuntu 18 but it not
strictly required.<br>
</div>
<div>2. Download and create a new desktop installation or
virtual machine with the system. Don't forget about our
hardware <a
href="https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements"
target="_blank" moz-do-not-send="true">requirements</a>!<br>
</div>
<div>3. Download our software verification framework:</div>
<div>sudo apt-get install git<br>
</div>
<div>git clone <a
href="https://github.com/ldv-klever/klever.git"
target="_blank" moz-do-not-send="true">https://github.com/ldv-klever/klever.git</a></div>
<div><br>
</div>
<div>4. Then follow <a
href="https://klever.readthedocs.io/en/latest/deploy_local.html"
target="_blank" moz-do-not-send="true">deployment steps</a>
for the local deployment. In particular modify
klever-minimal.json.sample and save it as klever.json in
$KLEVER_SRC/deployment/conf/ directory. Also set environment
variables to specify $KLEVER_SRC directory with Klever source
files and target installation directory $KLEVER_DEPLOY_DIR.
Then install Klever with the command:<br>
sudo $KLEVER_SRC/deploys/bin/deploy-local
--deployment-directory $KLEVER_DEPLOY_DIR install production<br>
</div>
<div><br>
</div>
<div>5. After Klever installation you can build the kernel and
create build base. <br>
</div>
<div><br>
</div>
<div>Download the kernel: <br>
</div>
<div>
<div>wget <a
href="https://cdn.kernel.org/pub/linux/kernel/v3.x/linux-3.14.79.tar.gz"
target="_blank" moz-do-not-send="true">https://cdn.kernel.org/pub/linux/kernel/v3.x/linux-3.14.79.tar.gz</a><br>
tar -xf linux-3.14.79.tar.gz<br>
<br>
</div>
<div>Install a suitable compiler:<br>
sudo update-alternatives --install /usr/bin/gcc gcc
/usr/bin/gcc-4.8 10<br>
sudo update-alternatives --config gcc</div>
<div>And choose 4.8 compiler there</div>
<div><br>
</div>
<div>Prepare your PATH environment variable:<br>
export PATH=$KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/:$PATH</div>
<div><br>
</div>
<div>Then run the following commands. It will take a lot of
time<br>
make allmodconfig<br>
clade-intercept make -j8 modules_prepare</div>
<div>clade-intercept -a make -j8 all</div>
<div>clade-all -p linux_kernel ./cmds.txt</div>
<div>echo "[\"$(readlink -f .)\"]" >
./clade/Storage/working source trees.json<br>
<br>
</div>
<div>6. Move this build base to another place. This is an
optional step but if you are going to build more bases in
this directory then it is better to do it. Note, then you
need a new base for each new configuration or kernel
version. <br>
</div>
<div>mv clade $NEW_PLACE/linux-3.14.79</div>
<div><br>
</div>
<div>7. Modify your deployment klever.json file in
$KLEVER_DEPLOY_DIR and add there a new section at the end of
the file in the root JSON object:<br>
"Klever Build Bases": ["$NEW_PLACE/linux-3.14.79"]</div>
<div><br>
</div>
</div>
</div>
</blockquote>
Here I need to specify a version, how to do it?<br>
<br>
Without version I get an error:<br>
<blockquote>
2018-11-08 10:13:30 (utils.py:099) ERROR> Version is not
specified for "Klever build bases"<br>
2018-11-08 10:13:30 (__init__.py:072) ERROR> Could not execute
action "update" for Klever "production" (analyze error messages
above for details)<br>
</blockquote>
<blockquote type="cite"
cite="mid:CAAGy8gnKdT4rmPwKnyXJzpYG1ZTYwiRr-MSSFwxiW5m99ZABPA@mail.gmail.com">
<div dir="ltr">
<div>
<div>Instead of $NEW_PLACE set an absolute path to the
directory with your build base.<br>
<br>
</div>
<div>8 Update the Klever installation:<br>
sudo $KLEVER_SRC/deploys/bin/deploy-local
--deployment-directory $KLEVER_DEPLOY_DIR update production<br>
<br>
</div>
<div>9. Now you can run verification.<br>
</div>
<div>
<div>Open localhost:8998 in the web browser.</div>
<div>Input username: manager, password: manager.</div>
<div>Click "Linux 3.14".</div>
<div>Click Job->Edit or ->Copy and edit job.json and
other files depending on your needs.</div>
<div>In the job.json set "build base": "linux-3.14.79" or an
another name if you named your build base differently.<br>
</div>
<div>Before running any large target such as all modules
first try to verify modules given with the example.<br>
</div>
</div>
</div>
</div>
</blockquote>
<blockquote type="cite"
cite="mid:CAAGy8gnKdT4rmPwKnyXJzpYG1ZTYwiRr-MSSFwxiW5m99ZABPA@mail.gmail.com">
<div dir="ltr">
<div>
<div>
<div>10. Click Decision->Start.</div>
<div>11. Click "Start" or "Start with default values".</div>
<div>13. Wait for verification results. It can take very
much time especially if your hardware isn't powerful
enough. <br>
</div>
<div><br>
If you will meet some issues, please, report them to us.
We will try to solve or workaround them together. Note
also, that we renamed some files, so there are some
differences from the Klever-1.1 version in job files.<br>
<br>
</div>
<div>Best,<br>
</div>
<div>Ilia Zakharov</div>
</div>
</div>
<br>
</div>
</blockquote>
Best,<br>
Vadim<br>
<blockquote type="cite"
cite="mid:CAAGy8gnKdT4rmPwKnyXJzpYG1ZTYwiRr-MSSFwxiW5m99ZABPA@mail.gmail.com">
<div dir="ltr"><br>
<div class="gmail_quote">
<div dir="ltr">ср, 17 окт. 2018 г. в 10:40, Evgeny Novikov
<<a href="mailto:novikov@ispras.ru"
moz-do-not-send="true">novikov@ispras.ru</a>>:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>Dear Ahmet,</div>
<div> </div>
<div>Your primary question will not be resolved in Klever
2.0. So, I will answer it.</div>
<div> </div>
<div>In the deployment documentation you can find <a
href="https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements"
target="_blank" moz-do-not-send="true">hardware
requirements</a>. I suggest that your VM does not meet
them, so, you either should empower it (I recommend this
to get better verification results faster) or use more
advanced settings. At page <a
href="http://localhost:8998/service/schedulers/"
target="_blank" moz-do-not-send="true">http://localhost:8998/service/schedulers/</a>
you can find the maximum amount of computer resources that
Klever can spend for solving verification jobs and
verification tasks. In the file you attached there are
restrictions on computer resources just for verification
jobs. But verification tasks are solved during solving
verification jobs, so you should also take into account
maximum computer resources that are allowed for
verification tasks. Usually they are much more than ones
for verification jobs! These resources are specified
within file "tasks.json" at the job page, say, <a
href="http://ldvdev:8998/jobs/5/" target="_blank"
moz-do-not-send="true">http://ldvdev:8998/jobs/5/</a>. I
hope that this is enough for you to proceed. </div>
<div> </div>
<div>For answering your second question it is definitely
necessary to wait for Klever 2.0 as it will be intended
for verification of C software rather than Klever 1.x that
can verify just Linux device drivers. But, please, do not
expect that Klever 2.0 will be able to verify some C
program without additional efforts. Our rich experience
and preliminary experiments show that one will need to
develop a suitable configuration and specifications for
each type of programs while verification tools like
CPAchecker do not handle unfamiliar code well sometimes.
If you are ready to invest much time, you are welcome! We
will be glad to hear some notes and remarks from you.</div>
<div> </div>
<div>-- </div>
<div href="http://mailto:novikov@ispras.ru">Evgeny Novikov<br>
Linux Verification Center, ISP RAS<br>
<a href="http://linuxtesting.org" target="_blank"
moz-do-not-send="true">http://linuxtesting.org</a></div>
<div> </div>
<div> </div>
<div> </div>
<div>17.10.2018, 09:12, "A. Celenk" <<a
href="mailto:ahmet.celenk@procenne.com" target="_blank"
moz-do-not-send="true">ahmet.celenk@procenne.com</a>>:</div>
<blockquote type="cite">
<div bgcolor="#FFFFFF">
<p>Hello Evgeny,</p>
<p>Thank you very much for Klever, and for your help. I
will be eagerly waiting for 2.0 release. Till then, I
may try to use the current version to learn some
basics. Here is what I have done:</p>
<p>I could reach the web interface and managed to login
as manager, and played around a little bit. Considered
the warning on the deployment tutorial about messing
up the computer, I have installed Klever on a Ubuntu
18.04 VM. Being a VM, it has low resources. I have
started the preset Linux 3.14 job with default
configurations and got "Given resource limits for job
and tasks in sum are too high, we do not have such
amount of resources" error. Then I have checked out
manual configuration and used "paranoid development"
preset configuration, and lowered the resources as
much as I can (see my attached configuration).
Nevertheless I am still getting the same error and it
fails.</p>
<p>Here are my questions for the current release; if
answers would greatly change for v2.0, just ignore
these and I will be waiting for the new one:</p>
<p> - Is it fine to use Klever in such a
low-resourced VM? If so, what my configurations should
be? If not, what are the minimum system requirements
for Klever?<br>
- How do I upload a new job (e.g. just a single C
file, or a project with makefile)?</p>
<p>Thank you again,</p>
<p>Regards,</p>
<p>Ahmet</p>
<div>On <span>16-10-2018 18</span>:00, Evgeny Novikov
wrote:</div>
<blockquote type="cite">Also, I would like to inform you
that in a couple of weeks we will release Klever 2.0
that will change very many things related with core
functionalities. If you have time, then I recommend to
wait for this release and try it rather than a version
that will be deprecated soon.<br>
<br>
16:08, 16 октября 2018 г., Evgeny Novikov <a
href="mailto:novikov@ispras.ru" target="_blank"
moz-do-not-send="true"><novikov@ispras.ru></a>:
<blockquote>
<div>
<div>16.10.2018, 13:55, "Evgeny Novikov" <<a
href="mailto:novikov@ispras.ru"
target="_blank" moz-do-not-send="true">novikov@ispras.ru</a>>:</div>
<blockquote type="cite">
<div>Hello Ahmed,</div>
<div> </div>
<div>Your question is absolutely right. Klever
lacks user documentation and I think that it
will not have it in a near future. So, if you
would like to proceed, most likely you will
have many questions.</div>
<div> </div>
<div>You shouldn't run any script to start
Klever if deployment was successful. You just
need to open localhost:8998 in your web
browser.</div>
</blockquote>
<div><br>
I forgot to mention that there are 3 users
created in advance:</div>
<ul>
<li>The first one is Administrator (login:
admin, password: admin) that can change user
privileges. Most likely you will not need it
unlike you are going to create a multiuser
setup.</li>
<li>The second one is Manager (login: manager,
password: manager). This user can almost
everything and you should start with it!</li>
<li>The third one is Service user that serves
for internal purposes.</li>
</ul>
<div> </div>
<blockquote type="cite">
<div> </div>
<div>If you will have any other questions,
please, ask us. We will be glad to get some
feedback from you.</div>
<div> </div>
<div>-- </div>
<div href="http://mailto:novikov@ispras.ru">Evgeny
Novikov<br>
Linux Verification Center, ISP RAS<br>
<a href="http://linuxtesting.org/"
target="_blank" moz-do-not-send="true">http://linuxtesting.org</a></div>
<div> </div>
<div> </div>
<div> </div>
<div>16.10.2018, 11:14, "A. Celenk" <<a
href="mailto:ahmet.celenk@procenne.com"
target="_blank" moz-do-not-send="true">ahmet.celenk@procenne.com</a>>:</div>
<blockquote type="cite">
<p>Hello,<br>
<br>
I will ask a dumb question: How do we run
Klever? I've completed the<br>
deployment; but couldn't figure out which
python script (or some other<br>
thing) should I run to start testing.<br>
<br>
P.S: I've used example
klever-minimal.json.sample as configuration
file.<br>
<br>
Thanks a lot,<br>
<br>
Ahmet Celenk<br>
<br>
<br>
_______________________________________________<br>
ldv-project mailing list<br>
<a
href="mailto:ldv-project@linuxtesting.org"
target="_blank" moz-do-not-send="true">ldv-project@linuxtesting.org</a><br>
<a
href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project"
target="_blank" moz-do-not-send="true">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a></p>
</blockquote>
</blockquote>
</div>
</blockquote>
</blockquote>
</div>
</blockquote>
_______________________________________________<br>
ldv-project mailing list<br>
<a href="mailto:ldv-project@linuxtesting.org"
target="_blank" moz-do-not-send="true">ldv-project@linuxtesting.org</a><br>
<a
href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project"
rel="noreferrer" target="_blank" moz-do-not-send="true">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a><br>
</blockquote>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
ldv-project mailing list
<a class="moz-txt-link-abbreviated" href="mailto:ldv-project@linuxtesting.org">ldv-project@linuxtesting.org</a>
<a class="moz-txt-link-freetext" href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a>
</pre>
</blockquote>
<p><br>
</p>
</body>
</html>