| 1 |
|
|---|
| 2 | <html>
|
|---|
| 3 | <body>
|
|---|
| 4 |
|
|---|
| 5 | <p>Welcome to CIVL, the Concurrency Intermediate Verification
|
|---|
| 6 | Language tool. CIVL is a Java project for verifying concurrent
|
|---|
| 7 | programs written in CIVL-C, which is a C dialect with extensions to
|
|---|
| 8 | concurrent language constructs. The CIVL project uses ABC, SARL and
|
|---|
| 9 | GMC. The CIVL tool can be used to perform a number of tasks, including
|
|---|
| 10 | the following:
|
|---|
| 11 | <ol>
|
|---|
| 12 | <li>preprocess or pass a CIVL-C program;</i>
|
|---|
| 13 | <li>verify a CIVL-C program;</li>
|
|---|
| 14 | <li>run a CIVL-C program;</li>
|
|---|
| 15 | <li>replay traces for a program.</li>
|
|---|
| 16 | </ol>
|
|---|
| 17 |
|
|---|
| 18 | In addition, it provides a framework for developing your own libraries
|
|---|
| 19 | or transformations on ASTs of various language extensions and
|
|---|
| 20 | libraries.
|
|---|
| 21 | </p>
|
|---|
| 22 |
|
|---|
| 23 | There is a simple command-line interface for CIVL (see {@link
|
|---|
| 24 | edu.udel.cis.vsl.civl.CIVL CIVL}), but most users will want to use CIVL
|
|---|
| 25 | through the user interface (see {@link
|
|---|
| 26 | edu.udel.cis.vsl.civl.run.IF.UserInterface UserInterface}). To use the API, it is helpful to have some
|
|---|
| 27 | understanding of the modular structure of CIVL. The CIVL source code is
|
|---|
| 28 | decomposed into modules, each with a well-defined interface and set of
|
|---|
| 29 | responsibilities. Some of these modules are decomposed further into
|
|---|
| 30 | sub-modules. The top-level modules are:
|
|---|
| 31 | <ol>
|
|---|
| 32 |
|
|---|
| 33 | <li><strong>util</strong>
|
|---|
| 34 | <ol>
|
|---|
| 35 | <li>responsibilities: simple general-purpose utility classes
|
|---|
| 36 | that do not use other parts of CIVL</li>
|
|---|
| 37 | <li>uses: nothing</li>
|
|---|
| 38 | <li>interface: {@link edu.udel.cis.vsl.civl.util.IF}</li>
|
|---|
| 39 | <li>entry point: none</li>
|
|---|
| 40 | </ol></li>
|
|---|
| 41 |
|
|---|
| 42 | <li><strong>transform</strong>
|
|---|
| 43 | <ol>
|
|---|
| 44 | <li>responsibilities: transformations of an AST</li>
|
|---|
| 45 | <li>uses: <strong>abc</strong></li>
|
|---|
| 46 | <li>interface: {@link edu.udel.cis.vsl.civl.transform.IF}</li>
|
|---|
| 47 | <li>entry point: CIVLTransform</li>
|
|---|
| 48 | </ol></li>
|
|---|
| 49 |
|
|---|
| 50 | <li><strong>run</strong>
|
|---|
| 51 | <ol>
|
|---|
| 52 | <li>responsibilities: parsing command line inputs and initial
|
|---|
| 53 | configurations of the tool</li>
|
|---|
| 54 | <li>uses: <strong>transform</strong>, <strong>abc</strong></li>
|
|---|
| 55 | <li>interface: {@link edu.udel.cis.vsl.civl.run.IF}</li>
|
|---|
| 56 | <li>entry point: UserInterface</li>
|
|---|
| 57 | </ol></li> TBC.
|
|---|
| 58 |
|
|---|
| 59 | </ol>
|
|---|
| 60 |
|
|---|
| 61 | </body>
|
|---|
| 62 | </html>
|
|---|
| 63 |
|
|---|
