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
Line 
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 dev.civl.mc.CIVL CIVL}), but most users will want to use CIVL
25 through the user interface (see {@link
26 dev.civl.mc.run.IF.UserInterface UserInterface}). To use the
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:
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>
39 <li>interface: {@link dev.civl.mc.util.IF}</li>
40 <li>entry point: none</li>
41 </ol></li>
42
43 <li><strong>config</strong>
44 <ol>
45 <li>responsibilities: static configurations of the system</li>
46 <li>uses: <strong>gmc</strong></li>
47 <li>interface: {@link dev.civl.mc.config.IF}</li>
48 <li>entry point: CIVLConfiguration</li>
49 </ol></li>
50
51 <li><strong>transform</strong>
52 <ol>
53 <li>responsibilities: transformations of an AST</li>
54 <li>uses: <strong>config</strong>, <strong>abc</strong>, <strong>sarl</strong></li>
55 <li>interface: {@link dev.civl.mc.transform.IF}</li>
56 <li>entry point: CIVLTransform</li>
57 </ol></li>
58
59 <li><strong>model</strong>
60 <ol>
61 <li>responsibilities: definitions of the control flow graph
62 representation of a CIVL-C program</li>
63 <li>uses: <strong>util</strong>, <strong>config</strong>, <strong>abc</strong>,
64 <strong>gmc</strong>, <strong>sarl</strong></li>
65 <li>interface: {@link dev.civl.mc.model.IF}</li>
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
74 dev.civl.mc.model.IF.expression}</li>
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
82 dev.civl.mc.model.IF.location}</li>
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
90 dev.civl.mc.model.IF.statement}</li>
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>
96 <li>interface: {@link dev.civl.mc.model.IF.type}</li>
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
103 dev.civl.mc.model.IF.variable}</li>
104 <li>entry point: none</li>
105 </ol></li>
106 </ol>
107 </li>
108 </ol></li>
109
110 <li><strong>state</strong>
111 <ol>
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>
116 <li>interface: {@link dev.civl.mc.state.IF}</li>
117 <li>entry point: States</li>
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>
126 <li>interface: {@link dev.civl.mc.log.IF}</li>
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>
136 <li>interface: {@link dev.civl.mc.dynamic.IF}</li>
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>
147 <li>interface: {@link dev.civl.mc.semantics.IF}</li>
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>
159 <li>interface: {@link dev.civl.mc.kripke.IF}</li>
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>
171 <li>interface: {@link dev.civl.mc.predicate.IF}</li>
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>
182 <li>interface: {@link dev.civl.mc.gui.IF}</li>
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>
192 <li>interface: {@link dev.civl.mc.library.IF}</li>
193 <li>entry point: none</li>
194 </ol></li>
195
196 <li><strong>run</strong>
197 <ol>
198 <li>responsibilities: parsing command line inputs and initial
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>
203 <li>interface: {@link dev.civl.mc.run.IF}</li>
204 <li>entry point: UserInterface</li>
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>
212 <li>interface: {@link dev.civl.mc}</li>
213 <li>entry point: CIVL</li>
214 </ol></li>
215
216 </ol>
217
218</body>
219</html>
220
Note: See TracBrowser for help on using the repository browser.