Project

General

Profile

Klever Components Overview » History » Version 8

Evgeny Novikov, 03/14/2016 11:07 AM

1 1 Evgeny Novikov
h1. Klever Components Overview
2
3 2 Evgeny Novikov
*Klever* consists of the following components (at the moment they are not clearly reflected in the repository):
4
* *Bridge*
5
* *Native Scheduler*
6
* *Cluster Scheduler*
7
* *VerifierCloud Scheduler*
8
* *Core*
9
* *Controller*
10 1 Evgeny Novikov
11 6 Evgeny Novikov
!Klever_Components_Scheme.png!
12
13 3 Evgeny Novikov
h2. Bridge
14
15 2 Evgeny Novikov
*Bridge* connects users and all other *Klever* components together by providing a web interface to a database. By using this interface users can prepare verification jobs of various classes (see below) and start their decision. Besides users can evaluate verification results by associating expert marks with corresponding reports (see below).
16 1 Evgeny Novikov
17 3 Evgeny Novikov
h2. Native and Cluster Schedulers 
18
19 8 Evgeny Novikov
Schedulers allocate available resources to execute verification jobs and verification tasks (see below) obtained from Bridge in accordance with their scheduling policy.
20 1 Evgeny Novikov
21 4 Evgeny Novikov
Both *Native Scheduler* and *Cluster Scheduler* have _Job Worker_ and _Task Worker_ as subcomponents. In case of *Native Scheduler* all instances of both workers are executed on the same computer as *Native Scheduler*. In case of *Cluster Scheduler* instances of workers can be executed on any computer of the cluster that has appropriate resources.
22 1 Evgeny Novikov
23 8 Evgeny Novikov
_Job Worker_ executes a verification job by means of the *Core* component. 
24 1 Evgeny Novikov
25 7 Alexey Khoroshilov
_Task Worker_ solves a verification task by means of a specified static verifier.
26 1 Evgeny Novikov
27 2 Evgeny Novikov
Both *Core* and static verifiers are launched under "BenchExec":https://github.com/sosy-lab/benchexec (at the moment for *Core* it is used RunExec that is a part of BenchExec) that counters and limits consumed resources and performs some common pre- and post-processing of input parameters and output results.
28 1 Evgeny Novikov
29 3 Evgeny Novikov
h2. VerifierCloud Scheduler
30
31 7 Alexey Khoroshilov
*VerifierCloud Scheduler* sends verification tasks to "VerifierCloud":http://vcloud.sosy-lab.org/. It cannot handle verification jobs.
32 1 Evgeny Novikov
33 3 Evgeny Novikov
h2. Core
34
35 8 Evgeny Novikov
*Core* handles a verification job. As a result of that several verification tasks can be prepared and submitted to Bridge. Besides *Core* and its subcomponents generate and upload reports including:
36 1 Evgeny Novikov
* unknown reports describing reasons of failures
37
* unsafe reports describing potential bugs in software found by static verifiers
38
* safe reports meaning that static verifiers can prove correctness of software against checked properties under corresponding conditions
39 2 Evgeny Novikov
* other auxiliary reports to provide information when *Core* and its subcomponents start/finish execution, what resources they consumed and so on
40 1 Evgeny Novikov
41 7 Alexey Khoroshilov
*Core* uses appropriate subcomponents to handle verification jobs of corresponding classes. In case of _Verification of Linux kernel modules_ they are:
42 5 Evgeny Novikov
* _Linux Kernel Build Command Extractor_ (_LKBCE_) fetches Linux kernel source code and then configures and builds the Linux kernel intercepting appropriate build commands, e.g. CC and LD commands
43
* _Linux Kernel Verification Object Generator_ (_LKVOG_) produces one or more verification objects that are trees of groups of source files with corresponding CC commands
44
* _Abstract Verification Task Generator_ (_AVTG_) weaves each generated verification object with rule specifications in the static verifier independent manner
45
* _Verification Task Generator_ (_VTG_) generates one or more verification tasks for a specified static verifier on the basis of each generated abstract verification task and performs post-processing of verification task decisions
46 1 Evgeny Novikov
47 5 Evgeny Novikov
_LKVOG_ has the following strategies to generate verification objects (at the moment they are not represented as corresponding subcomponents):
48 1 Evgeny Novikov
* Separate Linux Kernel Module (SLKM) - each verification object corresponds to a single Linux kernel module and consists of a single group of corresponding module source files with CC commands
49
50 5 Evgeny Novikov
_AVTG_ invokes plug-ins in the order and with special parameters specified by corresponding rule specifications. Each plug-in usually takes some specification(s) as input and can produces aspects or/and some data as output. Following plug-ins are available:
51
* _Source Analyser_ (_SA_) queries verification object source files to get some useful knowledge, e.g. information on function calls and definitions, macro substitutions, type and variable declarations (at the moment this knowledge is used just by EMG)
52
* _Environment Model Generator_ (_EMG_) generates environment models in form of aspects
53
* _Argument Signature Extractor_ (_ASE_) queries verification object source files to get argument signatures represented as strings allowing distinguish various objects like mutexes and spin locks 
54
* _Template Renderer_ (_TR_) renders specified templates on the basis of specified contexts, e.g. argument signatures
55
* _Rule Specification Generator_ (_RGG_) extends verification objects with rule model source files and add aspects binding them with verification object source files
56
* _Weaver_ weaves all produced aspects into verification object source files
57 1 Evgeny Novikov
58 5 Evgeny Novikov
_VTG_ has the following strategies to generate verification tasks:
59
* _All Bug Kind Merge_ (_ABKM_) considers all bug kinds specified in rule model source files as one and thus produces one verification task per each abstract verification task
60 3 Evgeny Novikov
61
h2. Controller
62 1 Evgeny Novikov
63 2 Evgeny Novikov
*Controller* performs various checks of available services and resources and notify concerned parties about this.