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*

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 distribute verification jobs and verification tasks (see below) to be decided on workers in accordance with available/required resources, priorities and so on. 

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_ decides a verification job with help of *Core*. 

_Task Worker_ decides a verification task with help 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* decides verification tasks by means of "VerifierCloud":http://vcloud.sosy-lab.org/. It can not decide verification jobs.

h2. Core

*Core* decides a verification job. During decision several verification tasks can be prepared. Besides *Core* and its subcomponents generate 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 decide 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 AVTG 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.