Common Deployment

To execute deployment scripts you need to install:

To deploy Klever one has to clone its Git repository (below a path to a directory where it is cloned is referred to as $KLEVER_SRC):

git clone --recursive https://forge.ispras.ru/git/klever.git

Then one has to get Klever Addons and perhaps Target Software. Both of them should be described appropriately within Deployment Configuration File.

Klever Addons

You can provide Klever Addons in various forms such as files, directories, archives or Git repositories. Deployment scripts will take care of their appropriate extracting. At the moment everything should be local, e.g. you can not specify an URL for a Git repository. The best place for Klever Addons is directory addons within $KLEVER_SRC (see Structure of Klever Git Repository).

Note

Git does not track $KLEVER_SRC/addons.

Klever Addons include the following:

CIF

One can download CIF binaries from here. These binaries are compatible with various Linux distributions since CIF is based on GCC that has few dependencies. Besides, one can clone CIF Git repository and build CIF from source using corresponding instructions.

CIL

CIL is a very legacy Klever addon. You can get its binaries from here. As well, you can build it from this source which has several specific patches relatively to the mainline.

Consul

One can download appropriate Consul binaries from here. We are successfully using version 0.9.2 but new versions can also be fine. It is possible to build Consul from source.

Verification Backends

You need at least one tool that will perform actual verification of your software. These tools are referred to as Verification Backends. As verification backends Klever supports CPAchecker well. Some other verification backends are supported experimentally and currently we do not recommend to use them. You can download binaries of CPAchecker suitable for checking most of requirements from here. For finding data races additionally download binaries of another custom version of CPAchecker from here. In addition, you can clone CPAchecker Git or Subversion repository and build other versions of CPAchecker from source referring corresponding instructions.

Optional Addons

If you are going to solve verification tasks using VerifierCloud, you should get an appropriate client. Most likely one can use the client from the CPAchecker verification backend.

Note

For using VerifierCloud you need appropriate credentials. But anyway it is an optional addon, one is able to use Klever without it.

Target Software

Like Klever Addons one can provide Target Software to be verified. At the moment this is only the Linux kernel. Providing source code of Target Software at this stage can quite considerably reduce overall verification time. The best place for Target Software is directory programs within $KLEVER_SRC (see Structure of Klever Git Repository).

Note

Git does not track $KLEVER_SRC/programs.

Deployment Configuration File

After getting Klever Addons and Target Software one needs to describe them within Deployment Configuration File. First we recommend to copy $KLEVER_SRC/deploys/conf/klever-minimal.json.sample to some JSON file within $KLEVER_SRC/deploys/conf/ (see Structure of Klever Git Repository). Since deployment scripts use $KLEVER_SRC/deploys/conf/klever.json by default this is the best place for that file.

Note

Git does not track $KLEVER_SRC/deploys/conf/*.json.

Note

$KLEVER_SRC/deploys/conf/klever-minimal.json.sample is so consize as possible. One can find much more examples for describing various entities in $KLEVER_SRC/deploys/conf/klever-deploy-means.json.sample

Then you need to fix the sample to describe Klever and all required Klever Addons and Target Software. Generally there are 3 pairs within Deployment Configuration File with names Klever, Klever Addons and Programs correspondingly. The first one directly represents a JSON object describing Klever. The second and the third ones are JSON objects where each pair represents a name of a particular Klever addon or Target Software and its description as a JSON object. There is the only exception. Within Klever Addons there is Verification Backends that serves for describing Verification Backends.

Each JSON object that describes an entity should always have values for version and path:

  • Version gives a very important knowledge for deployment scripts. Depending on values of this pair they behave appropriately. When entities are represented as files, directories or archives deployment scripts remember versions of installed/updated entities. So, later they update these entities just when their versions change. For Git repositories versions can be anything suitable for a Git checkout, e.g. appropriate Git branches, tags or commits. In this case deployment scripts checkout specified versions first. Also, they clone or clean up Git repositories before checkouting, so, all uncommited changes will be ignored. To bypass Git checkouting and clean up you can specify version CURRENT. In this case Git repositories are treated like directories.
  • Path sets either a path relative to $KLEVER_SRC or an absolute path to entity (binaries, source files, configurations, etc.). As we mentioned above you can specify individual files, directories, archives and Git repositories as paths.

For some Klever Addons it could be necessary to additionally specify executable path within path if binaries are not available directly from path. For Verification Backends there is also name with value CPAchecker. Keep this pair for all specified Verification Backends.

For Target Software you can additionally set copy .git directory and allow use local Git repository to True. In the former case deployment scripts will copy directory .git if one provides Target Software as Git repositories. This can be necessary for verifying commits from Git repositories. In the latter case deployment scripts will use specified Git repositories for cleaning up and checkouting required versions straightforwardly without cloning them to temporary directories.

Warning

Setting allow use local Git repository to True will result in removing all your uncommited changes! Besides, ignore rules from, say, .gitignore will be ignored and corresponding files and directories will be removed!

Note

You can prepare multiple deployment configuration files, but be careful when using them to avoid unexpected results due to tricky intermixes.

Note

Actually there may be more Klever Addons or Target Software within corresponding locations. Deployment scripts will consider just described ones.

Structure of Klever Git Repository

After Common Deployment the Klever Git repository can look as follows:

$KLEVER_SRC
├── addons
│   ├── cif-d95cdf0.tar.gz
│   ├── cil-1.5.1.tar.gz
│   ├── consul
│   ├── CPAchecker-1.6.1-svn ea117e2ecf-unix.tar.gz
│   ├── CPAchecker-1.7-svn 27946-unix.tar.gz
│   └── ...
├── deploys
│   ├── bin
│   │   ├── deploy-local
│   │   └── deploy-openstack
│   ├── conf
│   │   ├── klever.json
│   │   ├── klever-deploy-means.json.sample
│   │   └── klever-minimal.json.sample
│   └── ...
├── programs
│   ├── linux-3.14.tar.xz
│   ├── linux-stable
│   └── ...
└── ...