Architectures, Languages and Techniques
B.M. Cook (Ed.)
IOS Press, 1999

Printed in proceedings from the conference (p.19-36):
WoTUG-22. Architectures, Languages and Techniques for concurrent systems.
Edited by B.M.Cook.
ISBN 90 5199 480 X, 4 274 90285 4 C3000, ISSN 1383-7575.
IOS Press, NL: http://www.iospress.nl/ 

WoTUG 22
11-14 April 1999
Department of Computer Science
Keele University
UK
In charge: Barry M. Cook


Another side of SPoC:
occam's ALTer ego dissected with PC-lint

Řyvind TEIG
Navia Maritime AS, Division Autronica
7005 Trondheim, Norway
New address 2001

[Last updated: 25. september 2001 13:14]
This document obsoletes the printed version.

Changes after publication

Newest modification on top of list:

Abstract. 26500 lines of Standard C (ANSI C) generated from occam sources by the Southampton Portable occam Compiler (SPoC) has been analysed by the static analysis tool PC-lint. The target machine is a TMS320C32 DSP where all (the supported) C's primitive data types are mapped to 32 bit read and writes. This architecture stretches "ANSI" C quite a bit, but the "portable" occam compiler promised to handle it. Even if we had experienced no problems with the generated code and it compiled with all error handling enabled, we had to insert some 15-20 different global PC-lint filters plus local filters via in-line C in the occam sources. This was in addition to the base-level filters we also used for hand-written C. It kept PC-lint quiet, for individual C files as well as "global wrap up". By discussing each individual filter we arrive at the conclusion that none hid errors in the generated C. The analysis revealed a few points where the occam language definition could have been made stricter. We would like to PC-lint the generated sources with fewer messages disabled - changes to SPoC are therefore suggested. Altogether SPoC seems to have passed this test quite well. Even if we have no expertise to modify the (open) SPoC sources, this report could be considered as contributing to a prospective "Bazaar" development model - to bring forward an even more robust compiler for a portable and perhaps prospering occam language.

1. Introduction

Ego: mediator between the id, the superego, and the demands of society or reality [0]. Reality: Standard C. ALT: occam's version of a good teacher in a classroom of obedient pupils: watches for all raised arms and kindly processes one at a time without loosing any query. Alter ego: occam in C clothes.

The main goal of this article is to plough hands-on experience back to the caretakers of SPoC [1]. If the "bazaar" development & support model was used for SPoC, it could perhaps develop further than to the present regime of centralised bug-fixes [2]. During discussions of real-time Java an awakening of the interest in CSP, on which occam is based, seems to be present: "My crystal ball says that the next leap (or at least an upcoming leap) in software methodologies will be when someone comes up with a formalism that _really_ captures concurrent design, and when that formalism catches on (the way OO has). CSP is the most promising entrant I've seen so far."  (Bill Foote, Sun) [3]. We think it is important that occam (and implicitly a running subset of CSP) is available on any system that has a C compiler.

Les Hatton [4] argues first that Standard C is not good enough on its own and second, that it is good enough provided we use a set of coding conventions and verify the code with a static analysis tool, or do a combination of both static and dynamic analysis. This could perhaps be done by enabling all checks on a very strict C compiler, or by using separate tools. The occam community has argued that occam is good enough on its own, in the light of a stricter and more formal language definition, compiler-enforced and language-defined usage rules, and insertion of run-time checks when needed. Even if we cannot directly compare a parallel and a sequential language, we learnt that occam and C, with C mechanically generated and analysed, comprise a structure that could be used to improve on that structure's foundations. Occam could have some more usage checks defined, SPoC could generate even "better" C, and the static analysis tool could be used to verify SPoC's more than the generated C's correctness. Les Hatton is right that machine verified C programs are indeed trustworthy, our machine generated C securely monitors cargo on many of the world's oil- and gas tankers.

The product on which our software is running is the Autronica GL-100 radar-based fluid level gauge, comprising an embedded real-time system written in occam mixed with signal processing in Standard C. All code has been linked from a common native C level. The zigzag path that Autronica followed that ended with our using occam and SPoC, and how that experience has been, was described in [5]. [6] discusses more of the system's internal behaviour.

Legend. All non-proportional text at separate lines is either occam o:,   Standard C (hand-written or automatically generated) c:, PC-lint output p:, PC-lint options file P: or DOS-window commands d:. At some places we have chosen to number the lines. Example lines are x: y: z:.   File names are in italic.

2. Tools

2.1 SPoC

SPoC is an occam compiler that takes occam as input and generates Standard C. Our target processor is a Texas Instruments TMS320C32 DSP. In our case, all occam files are #INCLUDE-d into one "main" occam file, since we do not do SPoC separate compilation. Because of this SPoC only generates a single huge Standard C file. To do this SPoC needs two files, in addition to our occam sources:

occam2c.h - Macro file
Primitive data-types and macros. The file comes with SPoC, but we had to modify it slightly for the DSP.
occam2c.c - Runtime system
Timer interrupt, scheduler, communication functions etc. Mainly runnable code.
Contains slots where SPoC inserts compiler switches, a struct that contains all the statically defined data structures of all Standard C functions (reflecting occam high-level processes), and a main. This file also comes with SPoC, but we have added our own timer interrupt routine, special handling during power-up, error handling routines and stack test. End-of-DMA interrupt is also partly contained here.

In other words: "SPoC = consume my.occ with occam2c.h and occam2c.c to produce my.c."

2.2 PC-lint

The static analysis tool we used is the commercially available PC-lint by Gimpel Software. The manual [7] states that "PC-lint finds quirks, idiosyncrasies, glitches and bugs in C and C++ programs. The purpose of such analysis is to determine the potential problems in such programs prior to integration or porting, or to reveal unusual constructs that may be the source of subtle and, as yet, undetected errors. Because it looks across several modules rather than just one, it can determine things that a compiler cannot. It is normally much fuzzier about many details than a compiler wants to be." (p.4). A lint tool was first available in the Unix world. "Lint is named after the bits of fluff it supposedly picks from programs." (Free On-Line Dictionary Of Computing).

In order to run a C program through PC-lint we should ideally not have to do anything with our C code. But PC-lint addresses so many facets of the C programming language that we would have to inform about the fingerprints of the hardware on which the program is running. We do this with system-wide PC-lint commands. We may decide to code in such a way that PC-lint is not entirely happy, in this case we insert specific PC-lint filters to avoid the error, warning or information issued. The scope of such filters may be controlled: global, file, name (function, variable etc.), code block or single lines. We have used all these combinations in our verification. We also had to insert some PC-lint filters directly in the occam code, as in-line Standard C code.

PC-lint messages are numbered into groups:  1-153: syntax errors, 200-299: internal errors, 301-324: fatal errors, 401-670: warning messages, 701-806: information messages, 900-973: elective notes, 1001..: C++ messages.

We disable a PC-lint message by enabling a filter for that message (by number). Except for the explicitly enabled filters we use PC-lint default warning level of 3, meaning that we see all Errors, Warnings and Information messages.

PC-lint allows such filters (and commands) to be embedded in the source code by decorating any legal comment with lint and no leading space:  //lint ... or /*lint ...*/. This will be seen in the examples. Inlining these in occam is done by starting the line with #C (a non-portable SPoC feature).

In order to run PC-lint we use the following indirect command files. Files with a (-) are not discussed in this article, but for completeness, the files are listed in the Appendix.

std.lnt (-)
In our case it only lists the 3 next command files below.
co-ti320.lnt (-)
Defines hardware platform. Comes with PC-lint for the Texas DSPs, modified a little by us.
options.lnt (-)
Defines the global filters that we have decided to use for all Standard C, hand-written as well as generated by SPoC.
opt-syst.lnt
Defines global #defines as needed when we compile the system. Contains a reference to a hand-written assembly-file. Also, filters for machine-generated code not needed before PC-lint "global wrap-up".
myFiles.lnt (-)
Command file that contains a list of all the files we want to PC-lint, both machine-generated by SPoC and hand-written code.
occam2c.lnt
Filters for the single machine-generated file. This file is #include'd in SPoC's occam2c.c.

We also place filters directly into both occam2c.h, occam2c.c and in occam source files through in-line Standard C comments.

2.3 Texas Instruments Optimising C compiler

We compile the generated code with Texas Instruments' C compiler for TMS320C32 DSP [8], with all warning messages enabled through compiler option pw2 and no such messages issued - even before we started PC-lint'ing the system.

3. Some case studies

3.1 Replicated IF (warning 529, 644)

If in the FUNCTION IsEqualTo we remove the occam comment-chars -- in line 05, thereby adding an extra and unnecessary assignment, "isEqualTo_1476 may not have been initialised" (644) is avoided. Alternatively, we may add the occam in-line 05x to remove the message. By prefixing the occam variable with a $ SPoC will expand it, see line 09x in the Standard C listing.

o: 01 BOOL FUNCTION IsEqualTo (VAL []INT A, B) 

   02   BOOL isEqualTo:

   03   VALOF

   04     SEQ

   05       -- isEqualTo := FALSE

   05x      #C //lint -esym(644,$isEqualTo)

   06       IF

   07         IF i = 0 FOR (SIZE A)

   08           A[i] <> B[i]

   09             isEqualTo := FALSE

   10         TRUE

   11           isEqualTo := TRUE

   12     RESULT isEqualTo

   13 :

The generated code follows. We have added ?? where unimportant details have been removed and ??.. where we have just cut the line.

c: 01 static BOOL F_IsEqualTo_1479(tSF_P_M_GL100_m_gl100 *PP, ??..

   02 {

   03   BOOL _Result;

   04   tSF_F_IsEqualTo_1479 SF;

   05   tSF_F_IsEqualTo_1479 *FP = &SF;

   06   FP->Chain = PP;

   07   {

   08     BOOL isEqualTo_1476;

   09     {

   09x      //lint -esym(644,isEqualTo_1479) (o:05x)

   10       {

   11         INT i_1477;

   12         INT i_1477_End;

   13         i_1477 = 0;i_1477_End = i_1477 + (A_1474_Dim0);

   14         for (; i_1477 != i_1477_End; i_1477++)

   15         {

   16           if ((*((INT*)(((BYTE*)A_1474)+(RNGCHK(??)??..

   17           {

   18             isEqualTo_1476 = false; 

   19           }

   20           else

   21           {

   22             continue;

   23           }

   24           break;

   25         }

   26         if (i_1477 == i_1477_End) 

   27         if (true)

   28         {

   29           isEqualTo_1476 = true; 

   30         }

   31         else

   32         {

   33           SETERR(MSG_IF);

   34         } 

   34x        else {/*lint -unreachable */} // Our  

   35       }

   36     }

   37     _Result = isEqualTo_1476;

   38   }

   39   return _Result;

   40 }

(..We are still discussing why isEqualTo_1476 may not have been initialized.) The only possibility for the for-loop to be exited without an assignment is when the iterator has reached the end at the break statement - this is exactly what line 26 is catching. If SIZE (A_1474_Dim0) is zero and the for-loop is never run, line 26 will also catch it. So the loop-plus-line-26 is ok, it is the missing else statement after line 34 that is the problem. (We would wish a pair of curly brackets for the block in lines 28-34. This is the only place we have seen that SPoC has not decorated a block with curly brackets.) The only suggestion we have is to make PC-lint believe that the new else is unreachable, see line 34x. SPoC could change the layout of the code accordingly - with PC-lint comment and all (with a proper SPoC compiler option set). Alternatively, we could add occam line 05x - C line 09x. We are not certain whether this actually is an error in PC-lint - we have experimented with the for-loop, but have not succeeded in removing the warning. PC-lint admits that "When the checking for unutilised variables is first applied in a large mature project, there will be a small number of false hits" ([7] p.150). Warning 644 contains a "may" that is somewhat vague in this context and difficult to relate to.

We would also like SPoC, in the initialisation of i_1477_End, not to add a component with zero value.

There are more problems with the code above. The first parameter is meant to access variables that are in lexical scope to the function. Our function accesses no such variables, and the first parameter along with lines 4-6 are unnecessary. SPoC could be modified here so that it will not set up a non-used *PP , and we would have avoided the global "lint -save -esym(529,FP)" "FP not subsequently referenced" in file occam2c.lnt. In our generated code of 26500 lines this filter is used 23 times.

But how does PC-lint know that line 33 does not cause a missing assignment? We had to tell it to consider the semantics of seterr_ equal to the semantics of the standard function exit by wrapping the SETERR macro in file occam2c.h:

c: #define SETERR(M)\

     /*lint -save -function(exit,seterr_)*/ \

     seterr_ (M) \

     /*lint -restore*/

Aside: the macro RNGCHK also may end up in SETERR, but this is no problem for PC-lint.

3.2 Process skeletons: PC-lint argues over SPoC state machines

Occam's PAR handling, ALT processing, CHANnel communications and TIMER implementations (all process descheduling candidates) are implemented as C source state machines. These state machines are generated as a function of the occam constructs only and are out of the user's control.

3.2.1 Unreachable (warning 527)

o: 100 PROC Delay.ms (VAL INT DelayFor.ms)

   101   INT time:

   102   TIMER clock:

   103   SEQ

   104     clock ? time

   105     clock ? AFTER time PLUS DelayFor.ms

   106 :

1150 times in 26500 lines. The occam code above demands run-time system support that SPoC delivers:

c: 200 static void P_Delay_ms_1432 (tSF_P_Delay_ms_1432 *FP)

   201 {

   202   while(true)

   203   {

   204     switch(FP->_Header.IP)

   205     {

   206       CASE(0):  

   207         FP->time_1430 = ReadTimer();

   208         DELAY((FP->time_1430 + FP->DelayFor_ms_1429),1);

   209       CASE(1):  

   210         RETURN();

   211       default: SETERR(MSG_IP);

   212     }

   213   }

   214 }

PC-lint does not understand that all code above is in fact reachable: that Scheduler (in occam2c.c) later will schedule the code through a call to P_Delay_ms_1432 proper, with a new internal state. PC-lint protests on line 208 because the DELAY macro (below) contains a return to Scheduler. PC-lint also protests on line 210 because it does not know that the last parameter of the macro in line 208 is a next state specification. We have not seen that it is possible to tell PC-lint that there is a thread of control between the return in DELAY and CASE(1). Too bad, since erroneous unreachable code will not be detected with the filter enabled.

c: #define DELAY(t,l){FP->_Header.IP = l; WaitOnTimer(t); return;}

3.2.2. Label not referenced (warning 563)

995 times in 26500 lines. These messages refer to unused labels in the state machines. See lines 206 and 209 (above), PC-lint will warn that none of the labels are actually referred to. File occam2c.h defines CASE and GOTO (we compile with FASTGOTOS):

c: #ifdef FASTGOTOS

   #define CASE(x) case x: label_ ## x

   #define GOTO(x) goto label_ ## x;

   #else

   #define CASE(x) case x

   #define GOTO(x) {FP->_Header.IP = x;break;}

   #endif

PC-lint complains that label_0 and label_1 are not referenced. Compiling with FASTGOTOS undefined will solve the problem, but will compromise speed. Even if a non-referenced label is no problem, we suggest that SPoC instead differentiates and uses one of two macros instead of just one:

c: #define CASE(x) case x:

   #define CASEL(x) case x: label_ ## x

3.2.3 Control flows into case/default (warning 616)

1633 times in 26500 lines. PC-lint protests on line 209, see above. The reason is that there is no break statement after the previous line, and PC-lint does not know the semantics of the state-machine's primitives like DELAY. We tried to inform PC-lint that it should treat f.ex. DELAY as having exit semantics, but we did not succeed. In occam2c.h we tried to to add #define BREAK_ break:

c: #ifdef DO_BREAK

     #define BREAK_ break

     /*lint -save +fce -e309 : Continue on error, filter #error */

     #error DO_BREAK filters some PC-lint warnings 616, undef to create functional code!

     /*lint -restore */

   #else

     #define BREAK_

   #endif

We also added BREAK_ at the end of the following macros (only the ones where PC-lint protested, some more may exist). Observe that internally all the macros below alter program flow: line 'x' macros end with a return, line 'y' macro ends with a {..; break} and line 'z' macro is a goto. SPoC knows all this and uses them correctly.

x: INPUTx, OUTPUTx, ALTWT, DELAY, ENDP, WAITP, CALL, RETURN 

y: ALTEND

z: GOTO

Remember that, after all, we do wish to receive proper (616) warnings from other parts of the program. After the exercise above we discovered that we still needed the 616-filter. SPoC inserts individual state machine entries that just flows into next case for f.ex. this occam code:

o: IF

     a = b

       c := FALSE

     TRUE

       SKIP

In addition, SPoC also generates separate states for incrementing the counter value in a SEQ i=0 FOR N  loop and WHILE(i<N) loop's bottom code. SPoC code layout errors will not be spotted with the help of PC-lint's 616-warning, since we have to disable it. By inspecting every complaint with the filter disabled we did not find any such error - SPoC is a solid piece of code.

We do not actually see how SPoC could have "solved" this without adding extra run-time code to "correctly" enter next case. (Maybe this would be acceptable, though). Inserting the BREAK_ macro is dangerous since the program is left non-runnable, the inserted breaks severely disrupt some of the the macros modified to silent PC-lint.

SPoC state machine layout could be reconsidered after this PC-lint experience. We are however, reluctant to repairing things that do work. But we are also intrigued by the idea of leaving PC-lint warnings 527, 563 and 616 enabled.

3.3 Unused parameters (info 715)

Whenever an array is a parameter to an occam "function" (PROC or FUNCTION), in the generated code its size is always sent over along with a pointer to the array. Some times the occam program does not use this size. SPoC could be modified to clean up all non-used "size" parameters, after all they do take time to pass.

c: //lint -esym(715, Envelope_1909_Dim0)

The PC-lint filter above would filter correctly provided we could actually insert it without editing in the generated C source. The in-line C in occam will not be expanded as we would want it to, see first line below. Our suggestion is that SPoC allows a construct like this second line, even if unused sizes were removed it would be nice to have (now SPoC crashes with "invalid page fault"):

o: #C //lint -esym(715, SIZE $Envelope) // Not expanded

o: #C //lint -esym(715, $(SIZE Envelope)) // Suggestion

We have actually decided to use the value SIZE someArray on the rightmost side of a dummy assignment, to avoid a global filter for all "symbol not referenced" (715). 

3.4 Possible side effects in a macro (warning 574, 666)

This section describes a tour of how to satisfy PC-lint and shave off possible sources of error along the way.

o: INT FUNCTION AddressOf (VAL INT IOfSector) IS 

     IOfSector << FlashType[iOfFlashType][IOfShiftsToSector]:

The occam FUNCTION above was too much for PC-lint and warning 666 "expression with side effects passed to repeated parameter .. of macro" was issued:

p: _Result = LOGSHIFTLEFT(INT,IOfSector_2787,

     *((INT*)(((BYTE*)FP->Chain->Chain->Chain->FlashType_70)+

     (5*sizeof(INT))+(RNGCHK(FP->Chain->iOfFlashType_2742,5)*(7*sizeof(INT))))));

   m_gl100.c  13784  Warning 666: Expression with side effects passed to repeated

     parameter 3 in macro LOGSHIFTLEFT

The macro LOGSHIFTLEFT in file occam2c.h is:

c: #define LOGSHIFTLEFT(t,x,y) \

     /*lint -save -e574 */ \

     (((y)>=(sizeof(t)*BITS_PER_WORD))?0:((signed t)(((unsigned t)(x))<<(y))))\

     /*lint -restore */

The macro above shows that we, on a previous occasion had to insert the PC-lint filter 574 "signed-unsigned mix with relational" into the macro. In retrospect we chose to address that problem and change the macro to

c: #define LOGSHIFTLEFT(t,x,y) \

     (((y)>=((INT)(sizeof(t)*BITS_PER_WORD))) ? 0:\ 

     ((signed t)(((unsigned t)(x))<<(y))))

since we know that the sizeof operator can never return a value that exceeds the maximum int. This did not, of course, help the problem with the side effect. However, the problem was removed if RNGCHK was replaced by a constant (like 5). It turned out we had candidates for side effects because y is used twice in LOGSHIFTLEFT, and since the _Result assignment contains both LOGSHIFTLEFT and RNGCHK, PC-lint assumes this to potentially cause a side effect. With the actual parameters that SPoC sets up, no side effect does appear. However, since we need not do any test for shifts >= 32 (sizeof(t)*BITS_PER_WORD), we rewrote the macro, which is now:

c: #define LOGSHIFTRIGHT(t,x,y)((signed t)(((unsigned t)(x))>>(y)))

An interesting thing is that this macro is almost equal to one defined in occam2c.h and used when FAST_SHIFTS is defined, only the first signed should be introduced in that macro. At the end of the day we decided to keep both shaped-up macros, one that is side effect free and one that is not, and have FAST_SHIFTS defined instead.

4. Global filters

4.1 Constant value Boolean (warning 506)

903 times in 26500 lines. Coding with compile-time constants is a way to do general layout of C code, and we quite like it. Our compiler seems to always generate the minimally necessary code for such a construct. No change requested for SPoC.

c: if (4 * sizeof(INT) != BYTES_PER_WORD) failedtype="INT";

   if (true)

x: etc..

For SPoC generated code, this message is often paired with PC-lint info described in 4.10.

4.2 _setjmp not defined (warning 526)

1 time in 26500 lines. We had to inform PC-lint that we do not have a definition of the library prototype _setjmp. PC-lint knows that <setjmp.h> is a library header file and complains correctly because #define setjmp(_x) _setjmp(_x) is all setjmp.h says. Texas has left _setjmp in the air - they land it in the rst.src assembler file only. Good for the Texas system, bad diet for PC-lint. So we have to leave the "_setjmp(long *) not defined" (warning 526) filter in occam2c.lnt.

But this was not enough. In order not to receive altogether 3 complaints: "_setjmp undeclared, assumed to return int" (info 718), "call to _setjmp() not made in the presence of a prototype" (info 746) and global wrap-up message "no argument information provided for function _setjmp()" (info 628), we had to insert the second line in occam2c.h:

c: extern jmp_buf STOPP_env; // Was originally in occam2c.h

   extern int setjmp (jmp_buf);

4.3 FP  not subsequently referenced (warning 529)

23 times in 26500 lines. Documented in section 3.1.

4.4 Ignoring return value of rngchkub_ (warning 534)

108 times in 26500 lines. This one was easy to solve, we tried to remove the return parameter from the macro RNGCHKUB in file occam2c.h. It turned out that SPoC never used the return parameter, since RNGCHKUB was always used as the left-hand side of a comma operator. Our C reference specifies that ".. and the value of the left expression is discarded" [9] - i.e. SPoC uses the call only to crash on error. Filter 534 was not needed after all.

4.5 TMP not accessed (warning 550)

17 times in 26500 lines. This warning is issued for SPoC's layout of the occam ALT construct's tear-down code. We suggest that SPoC redefines the involved macros (in occam2c.h) and does a different layout. We do not understand why SPoC does it this way, but we assume that it either has to do with debugging or a historically different usage.

c: BOOL TMP = false;

   TMP |= DIST(4,(FP->allowNewInput_2291 == false),FP->time_2289);

   TMP |= DISS(5,((FP->waitingForAcknowledge_2288 == false) && (FP->noOfPackets_2287 > 0)));

   TMP |= DISC(6,true,FP->acknowledged_2285);

   TMP |= DISC(7,FP->allowNewInput_2291,FP->input_2284);

4.6 Loss of precision (info 713)

101 times in 26500 lines. PC-lint complains about conversions from unsigned int to a type that is signed. See section 4.8, the same solution goes.

4.7 while(1) ... (info 716)

154 times in 26500 lines. Replacing all while(true) with for(;;) will resolve this problem. PC-lint seems to think that the latter form is more acceptable. To be nice, SPoC could change.

4.8 Loss of sign in promotion from int to unsigned int (info 737)

619 times in 26500 lines. PC-lint here protests on converting the unsigned result of the sizeof operator to a signed value.

c: (INT*)(((BYTE*)FP->noOfPackets_2317)+(FP->i_2319*sizeof(INT)))) = 0;

As stated earlier, since we know that the sizeof operator can never return a value that exceeds the maximum int, there is no problem to cast to INT or signed. We propose that SPoC adds this cast. Better, it could use a SIZEOF macro, to be defined in occam2c.h like this:

c: #define SIZEOF(t) ((signed)sizeof(t))

PC-lint option -fzu (=sizeof-is-signed) could remove these messages, but it conflicts with typedef unsigned size_t  in the Texas system files Stddef.h, Stdio.h, Stdlib.hString.h and Time.h. This would need us to filter a "size_t not what was expected from fzu using type" (410). For conservative reasons we chose not to touch the Texas libraries. But they could have used signed, the compiler reported a "compiler error" at an array size of decimal 20,000,000, which is much less than maximum of even a signed 32 bit integer. Filter 737 is still active.

4.9 Unusual pointer cast (incompatible indirect types) (info 740)

50 times in 26500 lines. An occam RETYPES is converted to a C that PC-lint does not like. To state the PC-lint manual: "You can also suppress this message by first casting to char pointer or to void pointer but this is only recommended if the underlying semantics are right." SPoC checks RETYPES, so it should add a (void*) for the RETYPES construction (last line):

o: VAL []REAL32 Values RETYPES Array:

c: Values_2589 = (REAL32*)Array_2587;

c: Values_2589 = (REAL32*)(void*)Array_2587;

Occam abbreviations also some times (two dimensional array only?) end up with "incompatible indirect types", even if types are ok in the occam world. Fix: last line:

o: VAL [MAXE][LenNCR]INT Timeout IS [AntennaTempMissing]:

c: static INT TMP[1][3] = {{4,32,7}}; 

     FP->Timeout_3693 = (INT*)TMP;

c: FP->Timeout_3693 = (INT*)(void*)TMP;

And the implicit abbreviation picked out from a procedure call, with ok types in the occam world. No fix listed:

o: fileHandle:= FindFile ([fileName FROM 0 FOR len], fcb)

c: fileHandle_4232 = F_FindFile_4228(

     FP->Chain,len_4234,

     (BYTE*)((BYTE*)(((BYTE*)fileName_4233)+(

     (RNGCHKUB(0,len_4234,20),0)*sizeof(BYTE)))),1,30,(INT*)fcb_4235);

4.10 Boolean within 'if' always evaluates to True (info 774)

753 times in 26500 lines. This is just a slightly different version of "constant value Boolean"  in 4.1. No change requested for SPoC.

c: CHK(2==2,MSG_ASM)

c: if (!true) GOTO(9);

4.11 Line exceeds 600 characters (info 782)

1 time in 26500 lines. A line of length some 980 characters was produced. We have had a similar case fixed in an intermediate version of SPoC. Obviously it has not been fixed for all VAL expansions. This needs to be fixed more thoroughly. A warning report is also generated if the 793-filter is disabled, see 4.12.

o: VAL [NoOfFiles][MAXB.FILE.NAME]BYTE List IS ["..","..",..]

c: static BYTE TMP[13][20] = {{??,??,..},{??,??,..}};

   FP->List_1298 = (BYTE*)TMP;

4.12 ANSI limit .. exceeded -- processing is unaffected (info 793)

2 times in 26500 lines. The first warning "ANSI limit of 509 'characters in logical source line' exceeded -- processing is unaffected" (793) pops up at the line described in 4.11 when 782-filter is disabled.

The second warning is more interesting: "ANSI limit of 511 'external identifiers' exceeded -- processing unaffected" (793). Each time SPoC sees an occam VAL array IS it seems to generate a static (not "static" keyword used to limit scope, but static keyword as used to make cell placement permanent). PC-lint considers a static variable as external; our Texas linker for the DSP also assigns "global and static variables" to the same segment type (.bss).

o: VAL NCR.AllOK             IS [4,20,0]:

   VAL NCR.YouAreNotLoggedOn IS [4,30,1]:

c: {

     static INT TMP[3] = {4,20,0};

     FP->NCR_AllOK_1065 = (INT*)TMP;

   }

   {

     static INT TMP[3] = {4,30,1};

     FP->NCR_YouAreNotLoggedOn_1067 = (INT*)TMP;

   }

In the C lines above each TMP has its own memory segment - if not it would be meaningless to assign pointers to each of them.

SPoC does not have to make all of these static. Now every time, any place, we use an occam VAL array IS it costs us permanent storage, even if scope may be limited. SPoC could allocate these on the stack by removing the static word, provided the VAL was in lexical scope - and there was no descheduling in between, since the stack is not preserved between descheduling point. (Scheduler resides close to the bottom of the call tree, permanently above main. SPoC's scheduling is non-preemptive or co-operative.) Now, even a VAL array in a FUNCTION is declared static. Removing static on a 100 word array caused the executable segment (and no other segment except the non-tabulated stack) to be increased by 9 words - this is the price for a more complicated assignment. Another alternative, SPoC could have used the heap and a malloc statement, and declared the pointer as static. But this would also take run-time code and microseconds.

We do notice that the trade-offs done by the SPoC designers seem to be quite viable. We seem to be happy with SPoC left as it is. But it is a case for separate compilation - this would give us fewer static per module.

5. Generic solution not needed

We have previously discussed that SPoC sometimes inserts hooks for generic usage, but does not remove them when a less generic usage leaves the hooks unused (3.1). We have one more case:

5.1 Array not accessed (warning 550)

If we declare a VAL array and later reference only specific components of that array (or its SIZE), SPoC will pick out the true constant, and not use run-time initiated values. (We did not have any such array usage.) Example:  VAL Array IS [22,33,44]: and later usage of Array[1] will generate code where 33 is used. SPoC obviously does the right thing (for us), it is faster to use an in-instruction constant than initialising and indexing an array. Our compiler is smart enough not to generate any run-time code in this case, but the pointer to the array and the array are in fact allocated by the linker. The array pointer is even assigned to one of the few registers of the DSP. We suggest a clean-up job for SPoC here. SPoC seems to have taken a view that the C world should do cleaning (and it does to a remarkable degree), but this is not enough. We also suggest a new usage rule for occam as a consequence of this, see section 7.

6. Filters inserted in SPoC files

6.1 Macro file occam2c.h

6.2 Runtime system, file occam2c.c

7. occam revisited

During this project we have seen that the occam language, in our opinion, should be extended to include a few more rules for the compiler to enforce. The ST [10] compiler (and therefore also KRoC [11]) has implemented the following:

  1. name is not used
  2. Parameter name not used
  3. Routine name not used
  4. Name name descopes previous declaration

PC lint actually helps us enforce 1-4 above, since SPoC checks none of them. Learning from PC-lint, a couple of new rules could be applied (point 6 is inspired from section 5.1):

  1. Name name assigned, but not subsequently used
  2. Array name index index not used

Compiling the program below goes fine with SPoC, but PC-lint warns us (further down):

o: PROC Wish ()

     INT a, b, c:

     b := a

   :

p: Warning 530: a_3824 not initialized

   Warning 550: b_3825 not accessed

   Warning 529: c_3826 not subsequently referenced

8. Conclusions

We have arrived at several suggestions for minor modifications to SPoC code layout. Bear in mind that SPoC output already compiles with no errors or warnings by the Texas C compiler for TMS320C32. With the suggested modifications implemented, less PC-lint filters need be enabled, and PC-lint could to a larger extent be used to verify SPoC as well as our hand-written code. We also suggest a few more rules to apply for compilation of occam.

At time of writing Autronica has a support contract with Southampton University, who has placed the sources and compiled executables back at public domain. With the increasing interest in CSP, having an occam compiler being supported by many is thus technically possible. Users and compiler experts, in addition to the Southampton caretakers, should enlarge this already existing small bazaar.

Our plan now is to port 37000 lines of occam from an earlier transputer platform to a 386EX or AMD Élan™SC410 architecture, running under the VxWorks real-time operating system from WindRiver. We see this as a low-risk project.

Our occam2c.* and *.lnt files are available "as is" at: ftp://ftp.autronica.no/maritime/doc/wotug-22/wotug-22-aux.zip.

9. Document update

9.1 - PC-lint version 7.50p

We updated PC-lint to version 7.50p [7].

9.1.1 - lnt-files modifications

Only files co-ti320.lnt and options.lnt needed to be modified for the new version. (We updated PC-lint and Texas development system in one batch). Also, occam2c.lnt was modified, see next paragraph.

9.1.2 - Line exceeds Integer characters (error 91)

With 7.50p we had to introduce one more filter (and remove the old one, see below):

    static BYTE TMP[13][20] = {

    {102,115,101,114,118,58,92,73,95,66,117,102,102,101,114,46,100,97,116,32},

    {102,108,97,115,104,54,58,92,65,108,97,114,109,115,46,100,97,116,32,32},

    {102,108,97,115,104,54,58,92,84,97,110,107,46,100,97,116,32,32,32,32},

    {102,108,97,115,104,54,58,92,83,101,110,115,111,114,46,100,97,116,32,32},

    {102,108,97,115,104,54,58,92,86,111,108,117,109,101,46,100,97,116,32,32},

    {102,108,97,115,104,54,58,92,69,118,101,110,116,115,46,100,97,116,32,32},

    {102,108,97,115,104,120,58,92,65,108,9,114,109,115,46,104,97,116,32,32},

    {102,108,97,115,104,120,58,92,84,97,110,107,46,104,97,

m_gl100.c  26220  Error 91: Line exceeds 600 characters (use +linebuf)

This was caused by the following occam line:

VAL [NoOfFiles][C120.MAXB.FILE.NAME]BYTE NameOfFiles IS

      ["fserv:\I_Buffer.dat ",

       --

       "flash6:\Alarms.dat  ",

       "flash6:\Tank.dat    ",  -- 1K byte

       "flash6:\Sensor.dat  ",  -- 4.2 byte

       "flash6:\Volume.dat  ",  -- 5K byte

       "flash6:\Events.dat  ",

       --

       "flashx:\Alarms.hat  ",  -- File generetated by "Hat.java"

       "flashx:\Tank.hat    ",  -- -"-

       "flashx:\Sensor.hat  ",  -- -"-

       "flashx:\Volume.hat  ",  -- -"-

       "flashx:\Events.hat  ",  -- -"-

       "flashx:\prg_0512.bin",

       "runtm:\Boot1db_.bin "]:

This seems to have taken over the "e782 ........... Line exceeds 600 characters" message. We just replace e782 with e91 in occam2c.lnt. The reason for making a new number is probably the +linebuf option:

  1. Line exceeds Integer characters (use +linebuf) -- A line read from one of the input files is longer than anticipated. By default the line buffer size is 600 characters. By using the +linebuf option you can double this size. The size can be doubled ad infinitum.

We have no problem with the fact that this warning now has been defined as an error. As long as we don't have multiple expressions on a line, any truncated long line will be caught by the compiler. There will, at least, be a missing semicolon at the end of the line.

References

[0]
Electric Library. http://www.encyclopedia.com/ ("Psychoanalysis" paragraph)
[1]
Mark Debbage, Mark Hill, Sean Wykes, Denis Nicole, "Southampton's Portable Occam Compiler (SPOC)", In: Miles, Chalmers (ed.), "Progress in Transputer and occam Research", IOS Press, Amsterdam, 1994 (WoTUG 17 proceedings), pp.40-55. Also see http://www.hensa.ac.uk/parallel/occam/compilers/spoc/.
SPOC:Southampton's Portable Occam Compiler, Version 1.3b, Mon Sep 7 10:51:28 1998 M. Debbage, X. Fu, M. Hill, D. Nicole and S. Wykes University Of Southampton, ESPRIT GPMIMD P5404
On this quite new and intermediate version we had to run the generated source through a filter to replace all "Dim-" occurrences with "Dim_".
[2]
Eric S. Raymond, "The Cathedral and the Bazaar", 1998, http://www.redhat.com/redhat/cathedral-bazaar/cathedral-bazaar.html
[3]
Bill Foote, EmbeddedJava VM Group, Sun Microsystems. Archived at http://www.nist.gov/itl/div896/emaildir/rt-j/msg00312.html. Personal communication to The Requirements Working Group for Real-time Extensions for the Java™ Platform, National Institute of Standards and Technology, NIST.
Also see a "thread" discussing "Higher level Real-Time" starting at http://www.nist.gov/itl/div896/emaildir/rt-j/msg00285.html  
[4]
Les Hatton, "Safer C: Developing Software for High-integrity and Safety-critical Systems", 1994, McGRAW-HILL, ISBN-0-07-707640-0
[5]
Řyvind Teig, "PAR and STARTP Take the Tanks", In: P.H.Welch, A.W.P.Bakkers (ed.) "Architectures, Languages and Patterns for Parallel and Distributed Applications", pp. 1-18. 1998 (WoTUG 21 proceeding). IOS Press, Amsterdam, ISSN 1383-7575. Also see http://www.hensa.ac.uk/parallel/groups/wotug/wotug21/papers.html.
[6]
Řyvind Teig, "Non-preemptive occam in DSP real-time system", Real-Time Magazine, 3Q98. Also see http://www.realtime-info.be/encyc/magazine/98Q3/index983.htm
[7]
Gimpel Software, "PC-lint. A Diagnostic Facility for C and C++".  Manual is dated November 1995.
PC-lint for C/C++(NT) Ver.7.00p, Copyright Gimpel Software 1985-1997
See PC-lint version 7.50p, which prints:
PC-lint for C/C++(NT) Ver.7.50p, Copyright Gimpel Software 1985-1999
[8]
Texas Instruments TMS320C3x/C4x Optimizing C Compiler
TMS320C3x/4x C Compiler Shell Version 5.00
Copyright(c)1987-1997 Texas Instruments Incorporated
[9]
The C Programming Language. Kernighan and Ritchie. 2nd ed. 1988, p.209. ISBN 0-13-110362-8
[10]
SGS-Thomson, "occam 2.1 Toolset" , D7405, 1996. For transputers, now discontinued by ST Microelectronics. See [11].
[11]
KRoC, Kent Retargetable occam Compiler, see http://www.hensa.ac.uk/parallel/occam/projects/occam-for-all/kroc/index.html. Based on [10].

Appendix

File occam2c.lnt

Slightly modified (bold-faced) for PC-lint 7.50p:

#ifndef OCCAM2C_LNT_RESTORE_F

//lint -save -e506 ........... Constant value Boolean

//lint -save -e527 ........... Unreachable

//lint -save -e563 ........... Label not referenced

//lint -save -e616 ........... control flows into case/default

//lint -save -e713 ........... Loss of precision 

//lint -save -e716 ........... while(1) 

//lint -save -e737 ........... Loss of sign in promotion 

//lint -save -e740 ........... Unusual pointer cast (incompatible indirect types)

//lint -save -e774 ........... Boolean within 'if' always evaluates to ..

//lint -save  -e91 ........... 7.50p: Line exceeds 600 characters

//.... ..... -e782 ........... 7.00p: Line exceeds 600 characters

//lint -save -e793 ........... ANSI limit exceeded

//lint -save -esym(529,FP) ... FP not subsequently referenced

//lint -save -esym(550,TMP) .. not accessed

// ==========================================================================

// For module wrap-up (can only be filtered automatically at lnt-file level):

// --------------------------------------------------------------------------

//lint -save -esym(526,_setjmp) .. not defined

//.... ..... -esym(528,.......) .. not referenced:

//lint -save -esym(528,)

//lint -save -esym(528, MSG_AIM, MSG_ASM, MSG_ARM, MSG_CITL, MSG_EACF, MSG_EFROL)

//lint -save -esym(528, MSG_ELBCF, MSG_ERCF, MSG_EUBCF)

//lint -save -esym(528, MSG_I0_CODE_CKSUM_ERR, MSG_I1_CODE_CKSUM_ERR)

//lint -save -esym(528, MSG_ALBUM_ERR) // m_boot1.c only

//lint -save -esym(528, schedCnt, MSG_INT, MSG_SP)

//lint -save -esym(528, DONE_SETERR, ALLOCVEC, ChanIn2)

#endif

#ifdef OCCAM2C_LNT_RESTORE_F

//lint -restore 

//19 more -restore's

//lint -restore

#endif

Usage, top and bottom of occam2c.c:

top:    #include "OCCAM2C.LNT"

        #define   OCCAM2C_LNT_RESTORE_F

bottom: #include "OCCAM2C.LNT" // To catch restore's

File opt-syst.lnt

Not modified for PC-lint 7.50p:

-dASSERT_C

-dHATFILES_C

-dNO_BREAKPOINT_C

-dDO_BREAK

-esym(526, Get_StackStart) // Not defined

-esym(526, Get_StackSize)  // Not defined

// SPoC inhibitions not needed before global wrap-up

//    765 = could be made static

-esym(765, QTM, QBP, QFP, STOPP_env, Start_Process, CURTASK, TIMER)

-esym(765, Breakpoint, BlinkAndLeaveOn)

-esym(765, LON_Synch_Breakpoint, LON_Synch_Error_TryAgain)

-esym(765, Set_survivalFromLastRun, Get_survivalFromLastRun)

-esym(765, Set_survivalToDualPort_AndCopy)

File options.lnt

Slightly modified (bold-faced for PC-lint 7.50p (and a new version of the C-compiler):

-iC:\C3XTOOLS\INCLUDE

-iC:\USER\GL100\INCLUDE

-vf               // print name of all source files including header-files

+libclass(angle)  // library header-files specified with angle brackets

+libh(register.h) // define as library header

-e747 // significant prototype coercion (none in SPoC code)

-e783 // line does not end with new line

-e788 // enum constant not used within defaulted switch

-e537 // Repeated include file

-e749 // local enumeration constant not referenced

-e755 // global macro not referenced

-e756 // global typedef not referenced

-e757 // global declarator not referenced

-e758 // global enum not referenced

-e768 // global struct member not referenced (none in SPoC code)

-e769 // global enumeration constant not referenced

-esym(765, c_int09, c_int12) // could be made static

-esym(714, c_int09, c_int12) // not referenced

File co-ti320.lnt

Slightly modified (bold-faced for PC-lint 7.50p):

// Compiler Options for Texas Inst. TI320 class C compilers

	    // while processing compiler (library) header files ...

-wlib(1)      // sets the warning level within library headers to 1

-elib(553)  // suppress message about undefined preprocessor variables

-elib(652)  // suppress message about #define of earlier declared symbols

-elib(762)  // suppress message about multiple identical declarations and

-elib(760)  // suppress message about multiple identical macro defs

-sb32       // 'Byte' is 32 bits

-ss1        // short

-si1        // int

-sl1        // long

-sf1        // float

-sd1        // double

-sp1        // ptrs are 32 bits

-sc1        // char

-d_TMS320c30=1 // Pre-defined symbol indicates model 30

-esym(534,close,creat,fclose,fprintf,fputc)

-esym(534,fputs,fscanf,fseek,fwrite,lseek,memcpy,memmove,memset)

-esym(534,printf,puts,scanf,sprintf,sscanf,strcat,strcpy)

-esym(534,strncat,strncpy,unlink,write)

-emacro(???,va_arg) // the va_arg() macro can yield 415, 416, 661, 662

		    // 796 and 797 (out-of-bounds errors).

-emacro(413,offsetof)  // use of NULL pointer creates a stir

File std.lnt

co-ti320.lnt options.lnt opt-syst.lnt

Errata

Errata 1: SPoC helps with all 4 rules
In chapter "7 Occam Revisited" it says "PC lint actually helps us enforce 1-3 above". It should read "PC lint actually helps us enforce 1-4 above". It has been fixed in this document.
Rule 4 is covered by PC-lint with this message (example):
Warning 578: Declaration of 'pos_736' hides 'pos_736'