Project

General

Profile

Klever Components Overview » History » Version 5

Evgeny Novikov, 02/12/2016 01:38 PM

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 3 Evgeny Novikov
h2. Bridge
12
13 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).
14 1 Evgeny Novikov
15 3 Evgeny Novikov
h2. Native and Cluster Schedulers 
16
17 1 Evgeny Novikov
Schedulers distribute verification jobs and verification tasks (see below) to be decided on workers in accordance with available/required resources, priorities and so on. 
18
19 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.
20 1 Evgeny Novikov
21 4 Evgeny Novikov
_Job Worker_ decides a verification job with help of *Core*. 
22 1 Evgeny Novikov
23 4 Evgeny Novikov
_Task Worker_ decides a verification task with help of a specified static verifier.
24 1 Evgeny Novikov
25 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.
26 1 Evgeny Novikov
27 3 Evgeny Novikov
h2. VerifierCloud Scheduler
28
29 2 Evgeny Novikov
*VerifierCloud Scheduler* decides verification tasks by means of "VerifierCloud":http://vcloud.sosy-lab.org/. It can not decide verification jobs.
30 1 Evgeny Novikov
31 3 Evgeny Novikov
h2. Core
32
33 2 Evgeny Novikov
*Core* decides a verification job. During decision several verification tasks can be prepared. Besides *Core* and its subcomponents generate reports including:
34 1 Evgeny Novikov
* unknown reports describing reasons of failures
35
* unsafe reports describing potential bugs in software found by static verifiers
36
* safe reports meaning that static verifiers can prove correctness of software against checked properties under corresponding conditions
37 2 Evgeny Novikov
* other auxiliary reports to provide information when *Core* and its subcomponents start/finish execution, what resources they consumed and so on
38 1 Evgeny Novikov
39 2 Evgeny Novikov
*Core* uses appropriate subcomponents to decide verification jobs of corresponding classes. In case of _Verification of Linux kernel modules_ they are:
40 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
41
* _Linux Kernel Verification Object Generator_ (_LKVOG_) produces one or more verification objects that are trees of groups of source files with corresponding CC commands
42
* _Abstract Verification Task Generator_ (_AVTG_) weaves each generated verification object with rule specifications in the static verifier independent manner
43
* _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
44 1 Evgeny Novikov
45 5 Evgeny Novikov
_LKVOG_ has the following strategies to generate verification objects (at the moment they are not represented as corresponding subcomponents):
46 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
47
48 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:
49
* _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)
50
* _Environment Model Generator_ (_EMG_) generates environment models in form of aspects
51
* _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 
52
* _Template Renderer_ (_TR_) renders specified templates on the basis of specified contexts, e.g. argument signatures
53
* _Rule Specification Generator_ (_RGG_) extends verification objects with rule model source files and add aspects binding them with verification object source files
54
* _Weaver_ weaves all produced aspects into verification object source files
55 1 Evgeny Novikov
56 5 Evgeny Novikov
_VTG_ has the following strategies to generate verification tasks:
57
* _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
58 3 Evgeny Novikov
59
h2. Controller
60 1 Evgeny Novikov
61 2 Evgeny Novikov
*Controller* performs various checks of available services and resources and notify concerned parties about this.