The main aims and design principles of the OKlibrary

Articles on the OKlibrary:

• The report The OKlibrary: Introducing a "holistic" research platform for (generalised) SAT solving gives a general overview on the OKlibrary and its basic ideas as of December 2008.
• The journal version is The OKlibrary: Introducing a "Holistic" Research Platform for (Generalised) SAT Solving, which appeared in the journal Studies in Logic, 2009, volume 2(1), pages 20 - 53 (author Oliver Kullmann).

Outline

The OKlibrary is a research platform on generalised satisfiability and related fields, providing

• a computer-algebra based system (using Maxima/Lisp) for specification and prototyping,
• a generative C++ library (using modern C++),
• and extensions by external tools, including systems from logic, optimisation, statistics and discrete mathematics.

The library is open source (under GPLv3), and a strong integrated source control system yields full control over the development process.

Special services provided include:

• A powerful build system for compiling programs and running tests.
• An extensive documentation system, ranging from extracting program documentation to planning support.
• Installation and usage support for external packages, including tools used for programming and related activities.

Much emphasise is put on placing the development process in a wider context:

• The relations to neighbour fields, for example constraint satisfaction and graph theory, or complexity theory and automated theorem proving, are important, and collaboration shall be supported.
• Usage of existing software ("external sources") is strongly encouraged.
• A central problem in using external sources are the various dependencies which arise in this way, and the OKlibrary tries to lighten this burden by establishing a common environment for installation and usage.

To summarise:

1. The OKlibrary is an environment for attacking (allegedly) "intractable problems", with SAT in generalised form at its centre.
2. It aims at making accessible all related worlds from mathematics, informatics and software engineering.

The subject and its platform

"Generalised satisfiability" includes the following fields:

• Constraint satisfaction from the point of view of SAT, that is, with emphasise
  • on algorithms, not on language,
  • and on partial assignments and clauses for reasoning and learning algorithms.
  One might say, that
  1. SAT is considered as an abstract data type, for achieving "global intelligence",
  2. while CSP provides intelligent special methods for "local intelligence".
• Quantified extensions like QBF.
• Generalising clauses like in PB-solvers and SMT.
• Investigations into special structures (for example Ramsey-type problems).
• Any applications.

Important is the research character, and "purely" theoretical algorithms are welcome.

Though not "core business", many other areas are important for SAT, and thus are also integrated into the library:

• Logic
• Complexity theory
• Graph and hypergraph theory
• Combinatorics in general
• Algebra.

To avoid re-inventing many wheels, much emphasise is put on the use of external sources.

For supporting areas like statistics and numerical computation, powerful external systems are employed.

Modern C++, and generative and active libraries are of importance to overcome the split between efficiency and generality, and the library also undertakes practical research in these areas.

An integrated research environment

An open source library which supports research on such a variety of fields needs special means for collaboration:

• To support a wide range of research, the library is an "active library", and its full use means development within the framework.
• Compared with common "IDEs" ("integrated development environments"), the OKlibrary can be understood as an "IRE" ("integrated research environment").
• It is possible to use the library in the traditional way, as "include-and-link-only", but then many parts of the library are left out.
• The library provides means to develop within the library, but nevertheless to keep processes encapsulated.

A holistic library

The OKlibrary is a generative and active library, integrating services and activities traditionally not part of the delivered package and thus not easily usable:

• In this talk the general ideas of "holistic libraries", with emphasise on the higher order unit test system (see below), are outlined.
• A more complete account is found in this report .
• The general principle of active or generative libraries is, that all aspects of the programming process (like configuration knowledge) should be made available within the system (so that they become amenable to automation).
• We go beyond this level by including also planning and discussion (which are not amenable to automation).
• At the general level, only C++ is supported as a programming language, however for special purposes specialised languages have been selected.
  1. The discussion gives an overview on the design choices for the (formal) languages used in the OKlibrary.
  2. The integration with other programming languages (like Java) shall happen via the mechanism of external sources, which make available the source code and the compiled products, while the strength of C++ is exploited to be able to link with many other languages.
  3. Interfaces to other SAT libraries are important for the OKlibrary.

A remark on terminology: "generative" and "active" are used in the field of generative programming, while "holistic" is my (OK) own extended version of it. These notions are, in general and for our library, under active development.

The organisation of participation

The basic organisation principles for development are as follows:

• On the one hand we have the core distribution, over which the core development team has control, with me ("OK", that is, Oliver Kullmann) as the main developer and copyright holder.
  1. Strict coding standards and adherence to the design principles developed in the OKlibrary make interaction of the many different components possible.
  2. At the C++ level, the development process aims at full generality and genericity.
  3. At the Maxima/Lisp level, the development process aims at elegance and clarity combined with precision, avoiding "premature" abstraction.
  4. Prototypes in various forms are supported, but this within the framework of abstract ideas developed by the OKlibrary.
  5. Unity of the many theoretical and practical aspects of SAT is central to the OKlibrary, which concretely means that all components shall work together in one ("big") world --- through abstraction by generic and generative programming at the C++ level, by systematically developed conversions at the Maxima/Lisp level.
  6. The control over the core distribution includes strict control over version numbers (important for communicating the current standing).
  7. Plans and milestones at the core level can only be developed in close collaboration with the core development team.
  Thus development at the core level is under control,
  1. restricted by necessary adherence to general principles and ideas,
  2. which shall guarantee that the components admitted play together now and in the future.
• On the other hand we have the open space of the "virtual library" as a network of distributed clones:
  1. The anticipated development model for "normal" users is not the centralised submission to the core, but a decentralised model.
  2. Every external developer can take his clone of the OKlibrary as the centre of its own universe, where he and his team can play the same role as OK and his team for the core library.
  3. Essential is the idea of the OKlibrary as a "holistic library", which is open source taken to the maximum: Every user shall get the same possibilities as the core developers.
  4. If at some point the integration with the core library is wished, two basic models are considered:
     • Either by a concentrated joined effort the full integration into the core (which might make larger rewrites necessary).
     • Or the loose integration as an external source, with various forms of external testing applied.
     While at the core level a strong effort is undertaken to guarantee a high level of development, obviously this is not possible for external efforts --- which are then (obviously) free to do whatever they want.
  5. Clones of the OKlibrary which go public should make clear their heritage (besides what is given by the licence), but also should make clear the difference (which likely is in the interest of the external group).
  6. The history of the development of the OKlibrary, as reported by the source control system, is integral part of the OKlibrary.
     1. We expect that every external distribution of clones will respect the integrity of the history.
     2. If external distributions of clones present an incomplete or changed history, we will make strong efforts to make this publically known. If possible, also legal means might be used.
     3. Here "history" essentially refers to the history as presented by the source-code-management-system (Git in our case):
        • "completeness" means that the sequence of submissions is not interrupted;
        • "unchanged" means that the single submissions are unchanged.
        Git was chosen here since it provides cryptographic means for protecting the integrity of the history, and it is fast and powerful.
     4. The core development team makes a strong effort to guarantee the completeness of the history, so that every contribution, small or big, is visible in the history provided by the version control.

We should emphasise, that yet we do not have much experience with the "fractal nature" of the "network of clones" (with the OKlibrary as its original source), so a lot needs to be learned.

The public source-code repository

Technically, participation is organised as follows:

• At the public git repository the repository can be inspected.
• The git-address to clone from is "git://github.com/OKullmann/oklibrary.git".
• This is also the default when pulling from a repository built from a package.
• Collaboration happens with the help of Github as follows:
  1. A "fork" of the OKlibrary is created there.
  2. This fork is cloned at the local workspace of the developer, edited there, and pushed back to the fork at Github.
  3. Then the team at the original source is notified, and invited to pull the changes from the fork.
• See module "Buildsystem/SourceControl" for further information on the usage of Git.

On the release process

• To ease the start, packages containing everything related to the library are provided at the OKlibrary Internet page.
• On the average they appear once a weak, and are identified by a five-digit running number.
• These packages might also be used to update an existing installation, though in most cases
  1. pulling the changes from the main repository (just by using "git pull"),
  2. and updating the external sources by (selectively) downloading them from the OKlibrary Internet site,
  suffices.

The planning process

Central is the planning process:

1. Every action is announced by plans (in the corresponding plans-file), so that others know what's going on and can participate. Also only in this way the typical loss due to interruptions is avoided.
2. These plans are continuously evolved, so that before programming starts, a good "loose specification" is available.
3. Plans must be kept up-to-date, and also the corresponding milestone-entries.
4. So much of the planning process happens *within* the OKlibrary (not, as usual, somewhere else).
5. The history of the OKlibrary thus contains also all ("formalised") planning activities.
6. Mailinglists are for more informal discussions (finding out about interests, "chatting" about the plans (which is to be avoided in the plans-files)). So mailinglists are for "pre-discussion", and, potentially, "meta-discussions"; but as soon things concretise, they should move to the plans-files (only there they fully connect to the system).
7. To summarise, the planning process
   1. is somewhat similar to "patchwork", which comes in small pieces,
   2. is always in a somewhat well-defined state,
   3. and can be interrupted and continued as needed.
   This might be especially true for core developers, while external developers might prefer a more traditional model, where only at the end the distilled work (using the "cherry-picking" method preferred for example by the Git developers) is submitted. However, after some initial period of getting used to the continuous process of the OKlibrary, also external developers are encouraged to use the "continuous model" (and not the "batch model").

The testing process

• All code shall be accompanied by appropriate tests.
• Since most components are generic, "appropriate tests" means that actually test functions are to be provided, and this as part of the library.
• In this talk more general information about the "higher order unit test system" provided by the OKlibrary can be found.

Last modified: Sat Oct 29 21:11:32 BST 2011