This Sadl distribution (version 1.0b1) consists of a tar file containing Sadl tools for parsing and printing Sadl specifications, a tool for performing some simple syntactic checks on interpretations defined in mappings and patterns, and some documentation and examples. The idea is that, using these tools, you can check that Sadl hierarchies you define are syntactically correct.
This version of the distribution is for a Sun4 (a.k.a. SPARC) running SunOS4 (a.k.a. Solaris1). If you need to run Sadl on a different machine, let me know and maybe we can work something out.
The bad news is that the distribution is rather large, over 13M, and it prefers running on a machine with a fair amout of physical memory (say, at least 32M) and plenty of swap space. The good news is that it's the 90's, so your machine machine probably satisfies these requirements. Note that future releases of Sadl toolsets with greater functionality will not be much larger or require more memory.
The tools are easy to install and use. Installation consists of untarring the file, and setting the environment variable ALLEGRO_CL_HOME to point to the home/ directory from the tar file. So, assuming that you want to install in the current directory, the installation process might look something like this (with the parts you type in this font and the parts the system prints in this font):
% tar xvf sadl-distrinution.tar
sadl
home/
home/files.bu
home/4.3_xccxm2.lso
.
.
.
home/examples/ordering_to_signals.sadl
% setenv ALLEGRO_CL_HOME home
You'll probably also want to make sure that PATH is set so that sadl will be found if you attempt to start it from another directory, but that's up to you.
To run Sadl, you simply start up the executable at a shell prompt, supply a directory structure file name, and supply module names to be checked when you are prompted to do so. So the beginning of a session will look something like this:
% sadl
Allegro CL 4.3 [SPARC; R1] (11/1/96 15:52)
Copyright (C) 1985-1996, Franz Inc., Berkeley, CA, USA. All Rights Reserved.
*************************************
* *
* Welcome to Sadl tools (v. 1.0b1)! *
* *
*************************************
Enter name of file containing system directory structure:
Type in the name of the file containing the directory structure for the system you want to work with, which is just a list of directory names where Sadl will look for modules. The contents of a typical system directory structure file -- called, say, "my-system.txt" -- might look something like this:
"/usr/me/sadl/my-system/level1/" "/usr/me/sadl/my-system/mapping-1-to-2/" "/usr/me/sadl/my-system/level2/" "/usr/me/sadl/my-system/mapping-2-to-3/" "/usr/me/sadl/my-system/level3/" "/usr/me/sadl/my-system/patterns/"
This means that the files containing the modules of the system my-system are scattered among the six directories listed. Be careful not to omit the final slashes or the quotation marks!
The session that started above might continue as follows:
*************************************
* *
* Welcome to Sadl tools (v. 1.0b1)! *
* *
*************************************
Enter name of file containing system directory structure: my-system.txt
Enter name of Sadl module to be checked (or Q to quit):
(You might have to type in something like /usr/me/sadl/my-system/my-system.txt, if you didn't start sadl with /usr/me/sadl/my-system/ as the current directory.)
After this prompt, you simply type in the name of the Sadl module that you would like checked. Suppose that you wanted to check a pattern called channel_to_var. You might see the following result:
Enter name of Sadl module to be checked (or Q to quit): channel_to_var
Parsing and printing module in file "channel_to_var.sadl" ...
channel_to_var: PATTERN =
ABSTRACT_PATTERN ::
@m: ARCHITECTURE [->]
BEGIN
@f1: Functional_style!Function[-> @op: @t]
@f2: Functional_style!Function[@ip: @t ->]
@c: Dataflow_style!Channel<@t>
@a: CONNECTION =
Dataflow_style!Connects(@c, @op, @ip)
@@rest
END @m
CONCRETE_PATTERN ::
@m: ARCHITECTURE [->]
BEGIN
@f1: Functional_style!Function[->]
@f2: Functional_style!Function[->]
@v: Shared_Memory_style!Variable(@t)[->]
@a1: CONSTRAINT =
Shared_Memory_style!Writes(@f1, @v)
@a2: CONSTRAINT =
Shared_Memory_style!Reads(@f2, @v)
@@rest
END @m
ASSOCIATIONS ::
@op --> ()
@ip --> ()
@c --> (@v)
@a --> (@a1, @a2)
END channel_to_var
Applying the mapping check to module channel_to_var ...
Parsing module in file "channel_to_var.sadl" ...
MAP DOMAIN CHECK PASSED!
MAP TOTAL CHECK PASSED!
MAP RANGE CHECK PASSED!
With any luck, you will find any error messages you encounter in the mapping check to be self-explanatory. If you're having trouble with parsing, you might want to refer to the formal grammar for Sadl included in the doc/ subdirectory.
Note that the tools assume that the module channel_to_var is stored in a file called "channel_to_var.sadl" somewhere in the directory structure. The advantage of this scheme is clear if you consider checking a mapping from one architecture to another, where each architecture depends upon several style files, which in turn depend on other style files, and so on. Checking the correctness of the mapping requires examining all these other architecture and style modules. By organizing things so that sadl can find all the modules it needs when performing checks, the necessity of you somehow informing the system of the contents of those modules -- say, by checking them prior to checking the rule -- is eliminated.
The significance of the first check, that the module can be parsed, should be clear enough. The mapping check consists of three subchecks.
More sophisticated mapping checks -- for example, that the function defined by the associations determines an interpretation of the theory of the from-architecture in the theory of the to-architecture -- require translation of Sadl modules into logic. We expect that more robust versions of tools we have developed and are using internally to analyze the underlying logical representation of Sadl modules will be included in future releases of the Sadl toolset. But the checks provided in the current release prove surprisingly useful in practice: all four errors we have discovered in the original version of the patterns in our paper "Correct architecture refinement" were found by performing these three mapping subchecks.
If you have any problems, or just want to make some comments, feel free to send email to rar@csl.sri.com .