This repository has been archived by the owner on May 19, 2021. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
intro.html
34 lines (34 loc) · 2.34 KB
/
intro.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="icon" type="image/png" href="images/goblint_icon.png" />
<title>Goblint: Overview</title>
<link href="gobstyle.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="wrap">
<div id="head">
<div id="inst_logo">
<a href="http://www.cs.ut.ee/eng"><img src="images/TartuLogo.png" alt="Tartu Logo" width="27" height="40" /></a>
<a href="http://www.in.tum.de/en.html"><img src="images/TUMLogo.png" alt="TUM Logo" width="79" height="40" /></a>
</div>
<a href="index.html"><img src="images/goblint.png" alt="Goblint" width="225" height="37" id="goblint" /></a>
<ul id="navbar">
<li><a href="download.html">Download</a></li>
<li class="current">Overview</li>
<li><a href="docs.html">Papers</a></li>
</ul>
</div>
<div id="container">
<h2>Overview of Goblint Features</h2>
<p>Goblint is an analyzer of multi-threaded C programs. It computes a sound upper approximation of all possible thread interleavings using global invariants for shared data. The main application of this framework is for race detection. Goblint checks that all accesses to shared memory are protected by a common mutex.</p>
<p>The following screenshot illustrates the result of running the analyzer on a simple program with a static array of mutexes. </p>
<a href="images/screen.png" target="_self"><img src="images/screen.png" alt="Screenshot" width="720" height="522" class="screen" /></a>
<p>The safe incrementation function increases an element in the data array while acquiring the corresponding mutex; however, the main thread erroneously increments the third element while having locked the fourth lock.</p>
<p>As the example shows, Goblint not only tracks the flow of locks in and out of functions, but carefully considers the values and equalities between indexing variables to infer correlations. Additionally, Goblint is path-sensitive, so it deals with conditional locking schemes as well as possibly failing, interruptible and probing locking primitives. It also supports reader/writer locks.</p>
</div>
</div>
</body>
</html>