[ldv-project] Launching Klever
Vadim Mutilin
mutilin at ispras.ru
Fri Nov 9 13:00:25 MSK 2018
Thanks.
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.
Best,
Vadim
On 08.11.2018 23:57, Evgeny Novikov wrote:
> I hope that the issue is gone.
> There is https://forge.ispras.ru/issues/9369 that will help to avoid
> such the issues in future.
> --
> Evgeny Novikov
> Linux Verification Center, ISP RAS
> http://linuxtesting.org
> 08.11.2018, 13:17, "Vadim Mutilin" <mutilin at ispras.ru>:
>> 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 <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 <mailto: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/20181109/66ca9dd6/attachment.html>
More information about the ldv-project
mailing list