Klever

h1. Klever Components Overview

*Klever* consists of the following components (at the moment they are not clearly reflected in the repository):

* *Bridge*

* *Native Scheduler*

* *Cluster Scheduler*

* *VerifierCloud Scheduler*

* *Core*

* *Controller*

!Klever_Components_Scheme.png!

h2. Bridge

*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).

h2. Native and Cluster Schedulers 

Schedulers allocate available resources to execute verification jobs and verification tasks (see below) obtained from Bridge in accordance with their scheduling policy.

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.

_Job Worker_ executes a verification job by means of the *Core* component. 

_Task Worker_ solves a verification task by means of a specified static verifier.

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.

h2. VerifierCloud Scheduler

*VerifierCloud Scheduler* sends verification tasks to "VerifierCloud":http://vcloud.sosy-lab.org/. It cannot handle verification jobs.

h2. Core

*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:

* unknown reports describing reasons of failures

* unsafe reports describing potential bugs in software found by static verifiers

* safe reports meaning that static verifiers can prove correctness of software against checked properties under corresponding conditions

* other auxiliary reports to provide information when *Core* and its subcomponents start/finish execution, what resources they consumed and so on

*Core* uses appropriate subcomponents to handle verification jobs of corresponding classes. In case of _Verification of Linux kernel modules_ they are:

* _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

* _Linux Kernel Verification Object Generator_ (_LKVOG_) produces one or more verification objects that are trees of groups of source files with corresponding CC commands

* _Abstract Verification Task Generator_ (_AVTG_) weaves each generated verification object with rule specifications in the static verifier independent manner

* _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

_LKVOG_ has the following strategies to generate verification objects (at the moment they are not represented as corresponding subcomponents):

* 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

_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:

* _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)

* _Environment Model Generator_ (_EMG_) generates environment models in form of aspects

* _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 

* _Template Renderer_ (_TR_) renders specified templates on the basis of specified contexts, e.g. argument signatures

* _Rule Specification Generator_ (_RGG_) extends verification objects with rule model source files and add aspects binding them with verification object source files

* _Weaver_ weaves all produced aspects into verification object source files

_VTG_ has the following strategies to generate verification tasks:

* _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

h2. Controller

*Controller* performs various checks of available services and resources and notify concerned parties about this.