<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Thanks.<br>
<br>
The message has moved me on the dark side, but I've dressed the
build bases configuration smooth with cut file and managed to
proceed.<br>
<br>
Best,<br>
Vadim<br>
<br>
On 08.11.2018 23:57, Evgeny Novikov wrote:<br>
</div>
<blockquote type="cite"
cite="mid:13575141541710656@myt5-cf6d29327892.qloud-c.yandex.net">
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<div xmlns="http://www.w3.org/1999/xhtml">I hope that the issue is
gone.</div>
<div xmlns="http://www.w3.org/1999/xhtml"> </div>
<div xmlns="http://www.w3.org/1999/xhtml">There is <a
href="https://forge.ispras.ru/issues/9369"
moz-do-not-send="true">https://forge.ispras.ru/issues/9369</a>
that will help to avoid such the issues in future.</div>
<div xmlns="http://www.w3.org/1999/xhtml"> </div>
<div xmlns="http://www.w3.org/1999/xhtml">-- </div>
<div xmlns="http://www.w3.org/1999/xhtml"
href="http://mailto:novikov@ispras.ru">Evgeny Novikov<br>
Linux Verification Center, ISP RAS<br>
<a rel="noopener noreferrer" href="http://linuxtesting.org"
moz-do-not-send="true">http://linuxtesting.org</a></div>
<div xmlns="http://www.w3.org/1999/xhtml"> </div>
<div xmlns="http://www.w3.org/1999/xhtml"> </div>
<div xmlns="http://www.w3.org/1999/xhtml"> </div>
<div xmlns="http://www.w3.org/1999/xhtml">08.11.2018, 13:17,
"Vadim Mutilin" <a class="moz-txt-link-rfc2396E" href="mailto:mutilin@ispras.ru"><mutilin@ispras.ru></a>:</div>
<blockquote xmlns="http://www.w3.org/1999/xhtml" type="cite">
<div bgcolor="#FFFFFF">
<div>Hi Ilia!<br>
<br>
On 06.11.2018 18:50, Ilja Zakharov wrote:</div>
<blockquote type="cite"
cite="mid:CAAGy8gnKdT4rmPwKnyXJzpYG1ZTYwiRr-MSSFwxiW5m99ZABPA@mail.gmail.com">
<div>
<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.</div>
<div> </div>
<div>1. Choose your favorite Ubuntu/Debian image. The
instruction below is prepared for Ubuntu 18 but it not
strictly required.</div>
<div>2. Download and create a new desktop installation or
virtual machine with the system. Don't forget about our
hardware <a target="_blank" rel="noopener noreferrer"
href="https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements"
moz-do-not-send="true">requirements</a>!</div>
<div>3. Download our software verification framework:</div>
<div>sudo apt-get install git</div>
<div>git clone <a target="_blank" rel="noopener
noreferrer"
href="https://github.com/ldv-klever/klever.git"
moz-do-not-send="true">https://github.com/ldv-klever/klever.git</a></div>
<div> </div>
<div>4. Then follow <a target="_blank" rel="noopener
noreferrer"
href="https://klever.readthedocs.io/en/latest/deploy_local.html"
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</div>
<div> </div>
<div>5. After Klever installation you can build the kernel
and create build base.</div>
<div> </div>
<div>Download the kernel:</div>
<div>wget <a target="_blank" rel="noopener noreferrer"
href="https://cdn.kernel.org/pub/linux/kernel/v3.x/linux-3.14.79.tar.gz"
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>
</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> </div>
<div>Prepare your PATH environment variable:<br>
export
PATH=$KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/:$PATH</div>
<div> </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>
</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.</div>
<div>mv clade $NEW_PLACE/linux-3.14.79</div>
<div> </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> </div>
</div>
</blockquote>
Here I need to specify a version, how to do it?<br>
<br>
Without version I get an error:
<blockquote><span>2018-11-08 10</span>:13:30 (utils.py:099)
ERROR> Version is not specified for "Klever build bases"<br>
<span>2018-11-08 10</span>:13:30 (__init__.py:072) ERROR>
Could not execute action "update" for Klever "production"
(analyze error messages above for details)</blockquote>
<blockquote type="cite"
cite="mid:CAAGy8gnKdT4rmPwKnyXJzpYG1ZTYwiRr-MSSFwxiW5m99ZABPA@mail.gmail.com">
<div>
<div>Instead of $NEW_PLACE set an absolute path to the
directory with your build base.<br>
</div>
<div>8 Update the Klever installation:<br>
sudo $KLEVER_SRC/deploys/bin/deploy-local
--deployment-directory $KLEVER_DEPLOY_DIR update
production<br>
</div>
<div>9. Now you can run verification.</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.</div>
<div>Before running any large target such as all modules
first try to verify modules given with the example.</div>
</div>
</blockquote>
<blockquote type="cite"
cite="mid:CAAGy8gnKdT4rmPwKnyXJzpYG1ZTYwiRr-MSSFwxiW5m99ZABPA@mail.gmail.com">
<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.</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>
</div>
<div>Best,</div>
<div>Ilia Zakharov</div>
</div>
</blockquote>
Best,<br>
Vadim
<blockquote type="cite"
cite="mid:CAAGy8gnKdT4rmPwKnyXJzpYG1ZTYwiRr-MSSFwxiW5m99ZABPA@mail.gmail.com">
<div>
<div>ср, 17 окт. 2018 г. в 10:40, Evgeny Novikov <<a
rel="noopener noreferrer"
href="mailto:novikov@ispras.ru" moz-do-not-send="true">novikov@ispras.ru</a>>:</div>
<blockquote style="margin:0 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
target="_blank" rel="noopener noreferrer"
href="https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements"
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 target="_blank"
rel="noopener noreferrer"
href="http://localhost:8998/service/schedulers/"
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 target="_blank" rel="noopener
noreferrer" href="http://ldvdev:8998/jobs/5/"
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 target="_blank" rel="noopener noreferrer"
href="http://linuxtesting.org/"
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
target="_blank" rel="noopener noreferrer"
href="mailto:ahmet.celenk@procenne.com"
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><span>16-10-2018 18</span></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
target="_blank" rel="noopener noreferrer"
href="mailto:novikov@ispras.ru"
moz-do-not-send="true"><novikov@ispras.ru></a>:
<blockquote>
<div>
<div>16.10.2018, 13:55, "Evgeny Novikov" <<a
target="_blank" rel="noopener noreferrer"
href="mailto:novikov@ispras.ru"
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 target="_blank" rel="noopener
noreferrer"
href="http://linuxtesting.org/"
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
target="_blank" rel="noopener
noreferrer"
href="mailto:ahmet.celenk@procenne.com"
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 target="_blank" rel="noopener
noreferrer"
href="mailto:ldv-project@linuxtesting.org"
moz-do-not-send="true">ldv-project@linuxtesting.org</a><br>
<a target="_blank" rel="noopener
noreferrer"
href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project"
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 target="_blank" rel="noopener noreferrer"
href="mailto:ldv-project@linuxtesting.org"
moz-do-not-send="true">ldv-project@linuxtesting.org</a><br>
<a target="_blank" rel="noopener noreferrer"
href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project"
moz-do-not-send="true">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a></blockquote>
</div>
<pre>_______________________________________________
ldv-project mailing list
<a rel="noopener noreferrer" href="mailto:ldv-project@linuxtesting.org" moz-do-not-send="true">ldv-project@linuxtesting.org</a>
<a rel="noopener noreferrer" href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project" moz-do-not-send="true">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a>
</pre>
</blockquote>
<p> </p>
</div>
</blockquote>
</blockquote>
<p><br>
</p>
</body>
</html>