[ldv-project] Launching Klever
Vadim Mutilin
mutilin at ispras.ru
Thu Nov 8 13:17:19 MSK 2018
Hi Ilia!
On 06.11.2018 18:50, Ilja Zakharov wrote:
> Dear Ahmet,
>
> 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.
>
> 1. Choose your favorite Ubuntu/Debian image. The instruction below is
> prepared for Ubuntu 18 but it not strictly required.
> 2. Download and create a new desktop installation or virtual machine
> with the system. Don't forget about our hardware requirements
> <https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements>!
> 3. Download our software verification framework:
> sudo apt-get install git
> git clone https://github.com/ldv-klever/klever.git
>
> 4. Then follow deployment steps
> <https://klever.readthedocs.io/en/latest/deploy_local.html> 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:
> sudo $KLEVER_SRC/deploys/bin/deploy-local --deployment-directory
> $KLEVER_DEPLOY_DIR install production
>
> 5. After Klever installation you can build the kernel and create build
> base.
>
> Download the kernel:
> wget https://cdn.kernel.org/pub/linux/kernel/v3.x/linux-3.14.79.tar.gz
> tar -xf linux-3.14.79.tar.gz
>
> Install a suitable compiler:
> sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 10
> sudo update-alternatives --config gcc
> And choose 4.8 compiler there
>
> Prepare your PATH environment variable:
> export PATH=$KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/:$PATH
>
> Then run the following commands. It will take a lot of time
> make allmodconfig
> clade-intercept make -j8 modules_prepare
> clade-intercept -a make -j8 all
> clade-all -p linux_kernel ./cmds.txt
> echo "[\"$(readlink -f .)\"]" > ./clade/Storage/working source trees.json
>
> 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.
> mv clade $NEW_PLACE/linux-3.14.79
>
> 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:
> "Klever Build Bases": ["$NEW_PLACE/linux-3.14.79"]
>
Here I need to specify a version, how to do it?
Without version I get an error:
2018-11-08 10:13:30 (utils.py:099) ERROR> Version is not specified
for "Klever build bases"
2018-11-08 10:13:30 (__init__.py:072) ERROR> Could not execute
action "update" for Klever "production" (analyze error messages
above for details)
> Instead of $NEW_PLACE set an absolute path to the directory with your
> build base.
>
> 8 Update the Klever installation:
> sudo $KLEVER_SRC/deploys/bin/deploy-local --deployment-directory
> $KLEVER_DEPLOY_DIR update production
>
> 9. Now you can run verification.
> Open localhost:8998 in the web browser.
> Input username: manager, password: manager.
> Click "Linux 3.14".
> Click Job->Edit or ->Copy and edit job.json and other files depending
> on your needs.
> In the job.json set "build base": "linux-3.14.79" or an another name
> if you named your build base differently.
> Before running any large target such as all modules first try to
> verify modules given with the example.
> 10. Click Decision->Start.
> 11. Click "Start" or "Start with default values".
> 13. Wait for verification results. It can take very much time
> especially if your hardware isn't powerful enough.
>
> 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.
>
> Best,
> Ilia Zakharov
>
Best,
Vadim
>
> ср, 17 окт. 2018 г. в 10:40, Evgeny Novikov <novikov at ispras.ru
> <mailto:novikov at ispras.ru>>:
>
> Dear Ahmet,
> Your primary question will not be resolved in Klever 2.0. So, I
> will answer it.
> In the deployment documentation you can find hardware requirements
> <https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements>.
> 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
> http://localhost:8998/service/schedulers/ 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, http://ldvdev:8998/jobs/5/. I hope that this is enough for
> you to proceed.
> 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.
> --
> Evgeny Novikov
> Linux Verification Center, ISP RAS
> http://linuxtesting.org
> 17.10.2018, 09:12, "A. Celenk" <ahmet.celenk at procenne.com
> <mailto:ahmet.celenk at procenne.com>>:
>>
>> Hello Evgeny,
>>
>> 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:
>>
>> 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.
>>
>> 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:
>>
>> - 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?
>> - How do I upload a new job (e.g. just a single C file, or a
>> project with makefile)?
>>
>> Thank you again,
>>
>> Regards,
>>
>> Ahmet
>>
>> On 16-10-2018 18:00, Evgeny Novikov wrote:
>>> 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.
>>>
>>> 16:08, 16 октября 2018 г., Evgeny Novikov <novikov at ispras.ru>
>>> <mailto:novikov at ispras.ru>:
>>>
>>> 16.10.2018, 13:55, "Evgeny Novikov" <novikov at ispras.ru
>>> <mailto:novikov at ispras.ru>>:
>>>> Hello Ahmed,
>>>> 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.
>>>> You shouldn't run any script to start Klever if deployment
>>>> was successful. You just need to open localhost:8998 in
>>>> your web browser.
>>>
>>> I forgot to mention that there are 3 users created in advance:
>>>
>>> * 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.
>>> * The second one is Manager (login: manager, password:
>>> manager). This user can almost everything and you should
>>> start with it!
>>> * The third one is Service user that serves for internal
>>> purposes.
>>>
>>>> If you will have any other questions, please, ask us. We
>>>> will be glad to get some feedback from you.
>>>> --
>>>> Evgeny Novikov
>>>> Linux Verification Center, ISP RAS
>>>> http://linuxtesting.org <http://linuxtesting.org/>
>>>> 16.10.2018, 11:14, "A. Celenk" <ahmet.celenk at procenne.com
>>>> <mailto:ahmet.celenk at procenne.com>>:
>>>>>
>>>>> Hello,
>>>>>
>>>>> I will ask a dumb question: How do we run Klever? I've
>>>>> completed the
>>>>> deployment; but couldn't figure out which python script
>>>>> (or some other
>>>>> thing) should I run to start testing.
>>>>>
>>>>> P.S: I've used example klever-minimal.json.sample as
>>>>> configuration file.
>>>>>
>>>>> Thanks a lot,
>>>>>
>>>>> Ahmet Celenk
>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> ldv-project mailing list
>>>>> ldv-project at linuxtesting.org
>>>>> <mailto:ldv-project at linuxtesting.org>
>>>>> http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project
>>>>>
> _______________________________________________
> ldv-project mailing list
> ldv-project at linuxtesting.org <mailto:ldv-project at linuxtesting.org>
> http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project
>
>
>
> _______________________________________________
> 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/20181108/af49900d/attachment.html>
More information about the ldv-project
mailing list