source: CIVL/mods/dev.civl.mc/src/overview.html

main
Last change on this file was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 7.6 KB
RevLine 
[5563330]1
2<html>
3<body>
4
[45abec4]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>
[5563330]17
18 In addition, it provides a framework for developing your own libraries
[45abec4]19 or transformations on ASTs of various language extensions and
20 libraries.
[5563330]21 </p>
22
23 There is a simple command-line interface for CIVL (see {@link
[aad342c]24 dev.civl.mc.CIVL CIVL}), but most users will want to use CIVL
[45abec4]25 through the user interface (see {@link
[aad342c]26 dev.civl.mc.run.IF.UserInterface UserInterface}). To use the
[a01e883]27 API, it is helpful to have some understanding of the modular structure
28 of CIVL. The CIVL source code is decomposed into modules, each with a
29 well-defined interface and set of responsibilities. Some of these
30 modules are decomposed further into sub-modules. The top-level modules
31 are:
[5563330]32 <ol>
33
34 <li><strong>util</strong>
35 <ol>
36 <li>responsibilities: simple general-purpose utility classes
37 that do not use other parts of CIVL</li>
38 <li>uses: nothing</li>
[aad342c]39 <li>interface: {@link dev.civl.mc.util.IF}</li>
[5563330]40 <li>entry point: none</li>
41 </ol></li>
42
[411e0b8]43 <li><strong>config</strong>
44 <ol>
45 <li>responsibilities: static configurations of the system</li>
46 <li>uses: <strong>gmc</strong></li>
[aad342c]47 <li>interface: {@link dev.civl.mc.config.IF}</li>
[411e0b8]48 <li>entry point: CIVLConfiguration</li>
49 </ol></li>
50
[45abec4]51 <li><strong>transform</strong>
52 <ol>
53 <li>responsibilities: transformations of an AST</li>
[2fbc9e9]54 <li>uses: <strong>config</strong>, <strong>abc</strong>, <strong>sarl</strong></li>
[aad342c]55 <li>interface: {@link dev.civl.mc.transform.IF}</li>
[45abec4]56 <li>entry point: CIVLTransform</li>
57 </ol></li>
58
[a01e883]59 <li><strong>model</strong>
60 <ol>
61 <li>responsibilities: definitions of the control flow graph
62 representation of a CIVL-C program</li>
[16dc0b6]63 <li>uses: <strong>util</strong>, <strong>config</strong>, <strong>abc</strong>,
64 <strong>gmc</strong>, <strong>sarl</strong></li>
[aad342c]65 <li>interface: {@link dev.civl.mc.model.IF}</li>
[a01e883]66 <li>entry point: Models</li>
67 <li>submodules
68 <ol>
69 <li><strong>expression</strong>
70 <ol>
71 <li>responsibilities: definitions of various expressions of
72 CIVL</li>
73 <li>interface: {@link
[aad342c]74 dev.civl.mc.model.IF.expression}</li>
[a01e883]75 <li>entry point: none</li>
76 </ol></li>
77 <li><strong>location</strong>
78 <ol>
79 <li>responsibilities: definitions a location in the control
80 flow graph of a CIVL-C program</li>
81 <li>interface: {@link
[aad342c]82 dev.civl.mc.model.IF.location}</li>
[a01e883]83 <li>entry point: none</li>
84 </ol></li>
85 <li><strong>statement</strong>
86 <ol>
87 <li>responsibilities: definitions of various statements of
88 CIVL</li>
89 <li>interface: {@link
[aad342c]90 dev.civl.mc.model.IF.statement}</li>
[a01e883]91 <li>entry point: none</li>
92 </ol></li>
93 <li><strong>type</strong>
94 <ol>
95 <li>responsibilities: definitions of various types of CIVL</li>
[aad342c]96 <li>interface: {@link dev.civl.mc.model.IF.type}</li>
[a01e883]97 <li>entry point: none</li>
98 </ol></li>
99 <li><strong>variable</strong>
100 <ol>
101 <li>responsibilities: definitions of a variable of CIVL</li>
102 <li>interface: {@link
[aad342c]103 dev.civl.mc.model.IF.variable}</li>
[a01e883]104 <li>entry point: none</li>
105 </ol></li>
106 </ol>
107 </li>
108 </ol></li>
109
[16dc0b6]110 <li><strong>state</strong>
[a01e883]111 <ol>
[ce6859d]112 <li>responsibilities: creation and manipulation of states of a
113 CIVL model.</li>
114 <li>uses: <strong>config</strong>, <strong>model</strong>, <strong>gmc</strong>,
115 <strong>sarl</strong></li>
[aad342c]116 <li>interface: {@link dev.civl.mc.state.IF}</li>
[16dc0b6]117 <li>entry point: States</li>
[ce6859d]118 </ol></li>
119
120 <li><strong>log</strong>
121 <ol>
122 <li>responsibilities: data structures for logging errors during
123 verification.</li>
124 <li>uses: <strong>model</strong>, <strong>state</strong>, <strong>gmc</strong>,
125 <strong>sarl</strong></li>
[aad342c]126 <li>interface: {@link dev.civl.mc.log.IF}</li>
[ce6859d]127 <li>entry point: none</li>
128 </ol></li>
129
130 <li><strong>dynamic</strong>
131 <ol>
132 <li>responsibilities: general computations of symbolic
133 expressions, including the pretty printing method.</li>
134 <li>uses: <strong>util</strong>,<strong>model</strong>, <strong>state</strong>,
135 <strong>log</strong>, <strong>sarl</strong></li>
[aad342c]136 <li>interface: {@link dev.civl.mc.dynamic.IF}</li>
[ce6859d]137 <li>entry point: Dynamics</li>
138 </ol></li>
139
140 <li><strong>semantics</strong>
141 <ol>
142 <li>responsibilities: implementation of the semantics of
143 CIVL-C.</li>
144 <li>uses: <strong>util</strong>, <strong>config</strong>, <strong>model</strong>,
145 <strong>state</strong>, <strong>log</strong>, <strong>dynamic</strong>,
146 <strong>sarl</strong></li>
[aad342c]147 <li>interface: {@link dev.civl.mc.semantics.IF}</li>
[ce6859d]148 <li>entry point: Semantics</li>
149 </ol></li>
150
151 <li><strong>kripke</strong>
152 <ol>
153 <li>responsibilities: implementation of the semantics of
154 CIVL-C.</li>
155 <li>uses: <strong>util</strong>, <strong>config</strong>, <strong>model</strong>,
156 <strong>state</strong>, <strong>log</strong>, <strong>dynamic</strong>,
157 <strong>semantics</strong>, <strong>gmc</strong>, <strong>sarl</strong>
158 </li>
[aad342c]159 <li>interface: {@link dev.civl.mc.kripke.IF}</li>
[ce6859d]160 <li>entry point: Kripkes</li>
161 </ol></li>
162
163 <li><strong>predicate</strong>
164 <ol>
165 <li>responsibilities: definitions of predicates that are
166 required to hold for any CIVL-C programs.</li>
167 <li>uses: <strong>model</strong>, <strong>state</strong>, <strong>log</strong>,
168 <strong>dynamic</strong>, <strong>semantics</strong>, <strong>kripke</strong>,
169 <strong>gmc</strong>, <strong>sarl</strong>
170 </li>
[aad342c]171 <li>interface: {@link dev.civl.mc.predicate.IF}</li>
[ce6859d]172 <li>entry point: none</li>
173 </ol></li>
174
175 <li><strong>gui</strong>
176 <ol>
177 <li>responsibilities: graphical interfaces for viewing
178 counterexample traces.</li>
179 <li>uses: <strong>model</strong>, <strong>state</strong>, <strong>dynamic</strong>,
180 <strong>kripke</strong>, <strong>gmc</strong>, <strong>sarl</strong>
181 </li>
[aad342c]182 <li>interface: {@link dev.civl.mc.gui.IF}</li>
[ce6859d]183 <li>entry point: none</li>
184 </ol></li>
185
186 <li><strong>library</strong>
187 <ol>
188 <li>responsibilities: base implementation of libraries.</li>
189 <li>uses: <strong>model</strong>, <strong>state</strong>, <strong>log</strong>,
190 <strong>dynamic</strong>, <strong>semantics</strong>, <strong>kripke</strong>,
191 <strong>sarl</strong></li>
[aad342c]192 <li>interface: {@link dev.civl.mc.library.IF}</li>
[ce6859d]193 <li>entry point: none</li>
194 </ol></li>
[a01e883]195
[45abec4]196 <li><strong>run</strong>
197 <ol>
198 <li>responsibilities: parsing command line inputs and initial
[ce6859d]199 configurations of the tool.</li>
200 <li>uses: <strong>kripke</strong>, <strong>model</strong>, <strong>state</strong>,
201 <strong>transform</strong>, <strong>util</strong>, <strong>abc</strong>,
202 <strong>gmc</strong>, <strong>sarl</strong></li>
[aad342c]203 <li>interface: {@link dev.civl.mc.run.IF}</li>
[45abec4]204 <li>entry point: UserInterface</li>
[a01e883]205 </ol></li>
206
207 <li><strong>main</strong>
208 <ol>
209 <li>responsibilities: parsing command line inputs and initial
210 configurations of the tool</li>
211 <li>uses: <strong>run</strong></li>
[aad342c]212 <li>interface: {@link dev.civl.mc}</li>
[a01e883]213 <li>entry point: CIVL</li>
214 </ol></li>
[45abec4]215
[5563330]216 </ol>
217
218</body>
219</html>
220
Note: See TracBrowser for help on using the repository browser.