Contents
--------

1. What is gnatsync?
2. gnatsync parameters
3. Project support
4. Currently implemented checks
5. Processing of foreign threads
6. Output format

1. What is gnatsync?
   ------------------

gnatsync is the GNAT static analysis tool that helps to detect potential race
conditions in multitasking programs, by exposing the global data that is
accessed in unsynchronized manner by independent threads. As a threads
gnatsync considers Ada tasks and procedures that are defined as threads.

Input to gnatsync is a set of compilable Ada sources that constitutes a
complete program. As it output, the tool prints out a list of a data objects
for which potential unsynchronized access is detected, and for each such
object the tool provides a list of threads that access this object. Each
access is specified by a full sequence of subprograms calls when a given
thread does not reference the object directly.

gnatsync is an ASIS-based tool. It compiles the given sources to create the
corresponding tree files. All these compilations take place in a temporary
directory, which is created in the beginning of a gnatsync run and is deleted
when the processing of the argument sources is completed. If a source file
specified as gnatsync argument does not contain a legal Ada program unit, that
is to say if the program has syntactic of semantic errors, gnatsync cannot
process it. If the specified source contains an Ada unit which depends on Ada
units located in other directories, the user can either specify the source
search path by means of a -I option in '-cargs' section of gnatsync
parameters, in the same way as the source search path can be specified for
GNAT. This is not needed if gnatsync is called from the GNAT driver with the
corresponding project file.

2. gnatsync parameters
   -------------------

gnatsync has the following command-line interface:

 gnatsync [options] {filename} {-files=filename} [-cargs gcc_switches]

options:
 -a                 - process RTL units
 -d                 - debug mode
 -dd                - progress indicator mode (for use in GPS)
 -q                 - quiet mode (do not report results in Stdout)
 -v                 - verbose mode
 -t                 - output execution time
 -main=filename     - specify file containing main subprogram
 -threads=filename  - specify file describing foreign threads

 -o(s|m|f)          - output detalization level:
                      s - short, m(default) - medium, f - full
 -wq                - turn warnings off

 -out_file=filename - send output to filename

filename            - the name of the Ada source file to be analyzed.
                      Wildcards are allowed
-files=filemane     - the name of the text file containing a list
                      of Ada source files to analyze

gcc_switches        - a list of switches that are valid switches for gcc

3. Project support

gnasync can be applied to any set of sources, but it can produce useful and
complete results when called to a set of sources that make up a complete
program. The most convenient way to specify such a set of sources is a project
file. gnatsync can be called from the GNAT driver as other tools, so the most
practical way of invoking the tool is:

   gnat sync -Pproj -U [options]

4. Currently implemented checks
   ----------------------------

"Entry points" of the analysis performed by the tool are threads -  task
bodies and bodies of procedures defined as threads. The tool treats the
environment task as one more task to analyze (see section 10.2 of the Ada
Standard). If -main_ option is specified for the gnatsync call, gnatsync
treats it as the name of the source file containing the main subprogram. The
main  called by the environment task.

The purpose of the analysis is to identify references to the data objects
that are not local to the current thread (referred as simply "non local"
below). Four kinds of references are considered:

- direct read references;
- direct write references;
- indirect read references;
- indirect write references;

A direct reference is a reference in the code of a thread, excluding the
code of nested subprograms and tasks. An indirect reference is a reference
that appears in the body of some subprogram, called (directly or indirectly)
from a given thread. Read access is reading a value of a data object or a
component thereof; write access is updating a value of a data object or a
component thereof.

The tool analyzes non-local references to data objects from threads in order
to detect the following cases:

- a data object is written by one thread and read by a different thread;
- there is more than one thread that writes to the data object;

Note that these cases include a situation when a referred data object is local
for one of the thread that accesses it.

gnatsync makes the conservative assumption that there is more than one task
object (more then one thread) for each task type in the program. As a result,
a task type is considered as being distinct from itself, and any write access
to non-local data from the body of a task type is treated as a potentially
unsynchronized access.

If a thread has both direct and indirect access of the same (read/write)
kind to some data object, only the direct access is considered by the tool.

The following code is excluded from the analysis performed by the tool:

- generic declarations and generic bodies (note that the tool analyses the
  corresponding expanded spec and body of each instantiation);

- single task declarations and task type declarations (these contain no
  executable code).

- protected declarations and protected bodies;

- default initialization expressions in discriminant specifications,
  component declarations, and parameter specifications;

- code contained in critical sections, see the definition of a critical
  section in chapter 5 "Processing of foreign threads" below.

Call graph analysis
-------------------

To compute indirect references to non-local variables, gnatsync creates and
analyses the call graph of the program being analyzed. The call graph is
created with the following limitations:

- calls to protected operations are not considered;

- entry calls are not considered, because accept statements are critical (???)
  sections, and cannot lead to unsynchronized access. This design decision may
  be revised in the future, if it is perceived that the ordering of callers
  within an entry queue may be a source of non-determinism.

- only statically resolved calls are considered. That is, if a called
  subprogram is denoted by an access value, or if a call is a dispatching
  call, gnatsync generates a warning message to indicate that the analysis is
  of necessity incomplete, and does not examine further this call as a
  possible source of non-local access.

- implicit calls that are generated by evaluating default initialization
  expressions (discriminants, record components, omitted parameters in
  subprogram or entry calls) are not considered. This is a current limitation
  of the implementation that will be corrected in a future release.

- variable declarations having initialization expressions are not counted as
  write access. This initialization is a part of the elaboration of this data
  object, and in a legal program a data object cannot be accessed before its
  elaboration is completed.

Data object analysis
--------------------

As a data object, the tool considers only "whole" objects (that is - data
objects declared by object declarations), but not components of data objects.
Constant data objects are not considered. An access to an array component
is treated as an access to the whole array. In this context, a clever
quicksort algorithm that spawns two tasks to sort the two partitions of the
initial array will appear to have unsynchronized accesses, even though the
components accessed by the two tasks can be shown (with some effort) to
be disjoint.

If a pragma Atomic or a pragma Volatile is applied to a data object, such
object is not considered by the tool.

For data of an access type, we treat a dereference, i.e. a read or
modification of the designated object, as being a read/write of the access
value.

The following references are considered write references:

- a data object or a component thereof that appears as the left-hand side of
  an assignment statement;

- a data object or a component thereof that is an actual parameter
  corresponding to an OUT formal parameter;

The following references are considered as read and write references:

- a data object or a component thereof that is an actual parameter
  corresponding to an IN OUT formal parameter;

- a data object or a component thereof that is a prefix of an 'Access or
  an 'Unrestricted_Access attribute reference;

All other references are considered to be read references.

5. Processing of foreign threads
   -----------------------------
By default gnatsync analyzes only Ada threads (that is, Ada tasks) and does
not count (direct and indirect) references only in Ada critical sections (that
is, bodies of protected operations (what about statements inside accept
statements???). But a user can define foreign (that is, non-Ada) threads and
critical sections to be analyzed by the tool.

A foreign thread is an Ada procedure that is defined to be a thread. A foreign
critical section is a piece of a statement sequence that starts and ens with a
call to a specific subprograms that is defined to be procedures starting and
ending critical sections (such as to wait for a signal and to send a signal,
to seize a semaphore and to release a semaphore).

The definition of the foreign threads should be provided in a text file that
should be passed to the tool as a parameter of the '-threads' option.

A foreign thread is specified by providing a full expanded Ada name of the
corresponding procedure. Procedures that define critical sections are
specified by pairs, each pair defines a sparting and ending procedure for a
critical section. In the thread definition file, such a pair is specified as
two full expanded Ada names of starting and ending procedures enclosed by
braskets. Formally the syntax of the thread definition file can be described
as:

thread_deinition_file ::= {definition_element}
definition_Element ::= thread_definition | critical_section_definition
thread_definition ::= full_expanded_Ada_name
critical_section_definition ::= (full_expanded_Ada_name full_expanded_Ada_name)

The thread file hap free format (in respect of line breaks and speced) with
the only limitation that full_expanded_Ada_name cannot contain any white space
or line break. Ada-style comments are alloved (both comment lines and
end-of-line comments).

Here is an example of a thread definition file:

----------- start of thread definition file ---------------
--  Foreign threads
tasks.thread1
tasks.thread2

--  Critical sections
(Critical_Sections.Seize Critical_Sections.Release)
----------- end of thread definition file -----------------

A given start section subprogram may have more then one different end section
subprograms (and the other way around).

gnatsync does not make any cheaks that start and stop section subprograms are
used correctly from the point of view of controlling inter-process
communications. It allows nested and overlapping sections.

A program may have foreign critical section and does not have foreign threads,
and vise versa.

The current restrictions on the implementation of foreign threads are:

- only subprograms explicitly defined in the specs of the library packages can
  be used as foreign threads and critical section start/stop procedures;

- if a given package contains more then one (overloaded) subprograms with the
  name specified as a foreign thread or a critical section start/stop
  procedure, all these procedures are considered as foreign threads
  (start/stop procedures);

- all the subprogram full expanded names in a thread definition file should be
  different;

6. Output format
   -------------

By default the tool places the output in the file named 'gnatsync.out' that is
located in the current directory. You may specify the name of the output file
as the parameter of '-out_file' option (if a file with this name already
exists, it will be silently overriden).

There are three levels of the tool output, the needed level can be specified
with '-o<output_level> option.

Short output ('-os') contains only the names and source locations of the data
objects for that a potential unsynchronized access may take place.

Medium output ('-om', this is the default output level) provides for each data
object the list of threads that have access to this object. In case of a
direct access, the source location of this access is given. Threads that have
read and write access to this data object are listed separately.

Full output ('-of') provides for each indirect access the full backtrace
starting from the direct access to this object in some subprogram and ending
with the direct call to (this or another) subprogram in the thread body that
results in this access to the data object.

The tool analyzes the results of generic instantiations and reports cases of
potentially unsynchronized access to data objects for variables and thread
bodies defined in expanded generics. The source reference for entities and
data accesses in expanded generics is a chain of the source references
starting from the corresponding place in the code of generic unit and ending
with the instantiation place.

The tool also creates in the current directoy the file named 'gnatcync.log'
that contains a copy of all the diagnostic and tracing information.

Foreign threads
---------------
- All the full expanded Ada names of the threads, section start and section
  end procedures should be different;

- Critical section start/stop procedures are not analyzed;

- foreign critical sections may exist when there is no foreign threads, as
  well they can exist in tasks;