← Back to branch summary

~burner/xsb/debianized-xsb

« back to all changes in this revision

Viewing changes to examples/xmc/Rether/rether.xl

  • Committer: Michael R. Head
  • Date: 2006-09-06 22:11:55 UTC
  • Revision ID: burner@n23-20060906221155-7e398d23438a7ee4
Add the files from the 3.0.1 release package

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/xmc/Rether/rether.xl
 
1
%%----------------------------------------------------------------------
 
2
%%      rtf.xl
 
3
%%      Rether RTF version
 
4
%%      translated to XL by Yifei Dong
 
5
%%      October 1998
 
6
%%----------------------------------------------------------------------
 
7
 
 
8
%%----------------------------------------------------------------------
 
9
%       System constants
 
10
%       numNodes(NumberOfNodes).
 
11
%       maxID(NumberOfNodes-1).
 
12
%       TotalSlots(TotalTimeSlots).
 
13
%       maxRTSlots(TotalTimeSlots-1).
 
14
 
 
15
{*
 
16
config(NumNodes, TotalSlots) :-
 
17
        retractall(numNodes(_)),
 
18
        retractall(maxID(_)),
 
19
        retractall(totalSlots(_)),
 
20
        retractall(maxRTSlots(_)),
 
21
        abolish_all_tables,
 
22
        MaxID is NumNodes-1,
 
23
        MaxRT is TotalSlots-1,
 
24
        assert(numNodes(NumNodes)),
 
25
        assert(maxID(MaxID)),
 
26
        assert(totalSlots(TotalSlots)),
 
27
        assert(maxRTSlots(MaxRT)).
 
28
 
 
29
numNodes(4).
 
30
maxID(3).
 
31
totalSlots(3).
 
32
maxRTSlots(2).
 
33
*}
 
34
 
 
35
%%----------------------------------------------------------------------
 
36
%       ID arithmetic , Prolog Term
 
37
{*
 
38
incID(ID, NextID) :-
 
39
        numNodes(N),
 
40
        NextID is (ID+1) mod N.
 
41
*}
 
42
 
 
43
%%----------------------------------------------------------------------
 
44
%       Format of token
 
45
%       token(
 
46
%               ServingRealtimeFlag,
 
47
%               RealtimeModeBooleanArray,
 
48
%               RealtimeSlots,
 
49
%               NonRealtimeSlotsRemaining,
 
50
%               NextNonRealtimeNodeID
 
51
%       )
 
52
 
 
53
%%----------------------------------------------------------------------
 
54
%       Channel convention
 
55
%       input:  in(Port(ThisNode), Token)
 
56
%       output: out(Port(DestNode), Token)
 
57
 
 
58
%%----------------------------------------------------------------------
 
59
%       Node
 
60
%       States: ID
 
61
%               RealtimeMode (stored in token?)
 
62
 
 
63
 
 
64
node(Port, ID:integer) ::=
 
65
        Port? (ID, Token) o
 
66
        nodeActive(Port,ID,Token).
 
67
 
 
68
nodeActive(Port, ID:integer,Token) ::=
 
69
        Token = token(ServingRT, _RTMode, _RTSlots, _NRTAvail, _NextNRT) o
 
70
        if ServingRT == 1 
 
71
        then   {nodeRT(Port, ID,Token)}
 
72
        else   {nodeNRT(Port, ID, Token)}.
 
73
 
 
74
 
 
75
%%      RT action
 
76
%       1. optionally release realtime slot
 
77
%       2. pass token
 
78
 
 
79
nodeRT(Port,ID:integer,Token) ::=
 
80
        action(rt(ID)) o
 
81
        { releaseRT(ID,Token,Token1) 
 
82
        # Token1 = Token
 
83
        } o
 
84
        findNextNodeRT(ID, Token1, Next, NewToken) o
 
85
        if Next == ID then
 
86
                {% no token passing within the same node
 
87
                nodeActive(Port,ID,NewToken)}
 
88
        else    {Port! (Next,NewToken) o
 
89
                node(Port,ID)}.
 
90
 
 
91
%% Prolog Term
 
92
{*
 
93
releaseRT(ID, Token, NewToken) :-
 
94
        Token = token(ServingRT, RTMode, RTSlots, NRTAvail, NextNRT),
 
95
        ( RTSlots > 1
 
96
        ->      (NewRTSlots is RTSlots-1,
 
97
                 resetbit(RTMode, ID, NewRTMode),
 
98
                 NewToken = token(ServingRT, NewRTMode, NewRTSlots,
 
99
                                  NRTAvail, NextNRT))
 
100
        ;       NewToken = Token).
 
101
 
 
102
findNextNodeRT(ID,Token,Next,NewToken) :-
 
103
        Token = token(_ServingRT, RTMode, RTSlots, NRTAvail, NextNRT),
 
104
        ID1 is (ID + 1),
 
105
        (0 is (RTMode >> ID1)
 
106
        ->      % no more RT node, then pass token to NRT node
 
107
                (Next = NextNRT,
 
108
                NewToken = token(0, RTMode, RTSlots, NRTAvail, NextNRT))
 
109
        ;       (firstTrue(RTMode,ID1,Next),
 
110
                NewToken = Token)
 
111
        ).
 
112
*}
 
113
 
 
114
%%      NRT action
 
115
%       1. optionally reserve realtime slot
 
116
%       2. pass token
 
117
 
 
118
 
 
119
nodeNRT(Port, ID:integer, Token) ::=
 
120
        action(nrt(ID)) o
 
121
        {reserveRT(Port, ID, Token, NewToken)
 
122
        # NewToken = Token
 
123
        } o passTokenNRT(Port,ID,NewToken).
 
124
 
 
125
reserveRT(Port, ID:integer, Token, NewToken) ::=
 
126
        Token = token(ServingRT, RTMode, RTSlots, NRTAvail, NextNRT) o
 
127
        maxRTSlots(MaxRT) o
 
128
        if (falsebit(RTMode, ID) /\ RTSlots < MaxRT) then
 
129
                {NewRTSlots is RTSlots+1 o
 
130
                 setbit(RTMode, ID, NewRTMode) o
 
131
                 NewToken = token(ServingRT, NewRTMode, NewRTSlots,
 
132
                                  NRTAvail, NextNRT) o
 
133
                 action(reserve(ID))}
 
134
        else    {NewToken = Token}.
 
135
 
 
136
passTokenNRT(Port, ID:integer,Token) ::=
 
137
        Token = token(ServingRT, RTMode, RTSlots, NRTAvail, NextNRT) o
 
138
        incID(NextNRT, NewNextNRT) o
 
139
        NewNRTAvail is NRTAvail - 1 o
 
140
        if NewNRTAvail > 0
 
141
        then    % if NRT slots are available,
 
142
                % pass the token to the next NRT ndde
 
143
                {NewToken = token(ServingRT, RTMode, RTSlots, 
 
144
                                NewNRTAvail, NewNextNRT) o
 
145
                Port! (NewNextNRT, NewToken) o
 
146
                node(Port,ID)}
 
147
        else    % if NRT slots are used up,
 
148
                % end this cycle and start a new cycle
 
149
                {action(endcycle) o
 
150
                totalSlots(Slots) o
 
151
                ResetNRTAvail is Slots - RTSlots o
 
152
                NewToken = token(1, RTMode, RTSlots,
 
153
                                ResetNRTAvail, NewNextNRT) o
 
154
                firstTrue(RTMode, 0, FirstRT) o
 
155
                action(startcycle) o
 
156
                if FirstRT == ID then
 
157
                        % no token passing within the same node
 
158
                        {nodeActive(Port,ID, NewToken)}
 
159
                else    {Port! (FirstRT, NewToken) o
 
160
                        node(Port,ID)}
 
161
                }.
 
162
 
 
163
%%----------------------------------------------------------------------
 
164
%       generator
 
165
%       1. creates the array of nodes
 
166
%       1. marks the starting of the first cycle
 
167
%       2. generates the token
 
168
/*
 
169
generator(N:integer) ::=
 
170
        if  N > 0 then
 
171
                {N1 is N-1 o
 
172
                {generator(N1) | node(Port,N1)}}
 
173
        else    {action(startcycle) o
 
174
                totalSlots(Slots) o
 
175
                NRTSlots is Slots-1 o
 
176
                out(Port(0), token(1,1,1,NRTSlots,0)) o
 
177
                end}.
 
178
*/
 
179
%%----------------------------------------------------------------------
 
180
%       System specification
 
181
/*
 
182
rether ::=
 
183
        numNodes(N) o
 
184
        (generator(N) \ { Port(_) }).
 
185
*/
 
186
starter(Port) ::=
 
187
        action(startcycle) o
 
188
        Port !(0, token(1,1,1,2,0)) o
 
189
        end.
 
190
 
 
191
rether ::=
 
192
          starter(Port)
 
193
        | node(Port,0)
 
194
        | node(Port,1) 
 
195
        | node(Port,2)
 
196
        | node(Port,3).
 
197
 
 
198
%%----------------------------------------------------------------------
 
199
%       Boolean array arithmetics
 
200
 
 
201
{*
 
202
truebit(Array, Bit) :-
 
203
        1 is ((Array >> Bit) mod 2).
 
204
 
 
205
falsebit(Array, Bit) :-
 
206
        0 is ((Array >> Bit) mod 2).
 
207
 
 
208
setbit(Array, Bit, NewArray) :-
 
209
        truebit(Array, Bit)
 
210
        ->      NewArray = Array
 
211
        ;       NewArray is Array + (1 << Bit).
 
212
 
 
213
resetbit(Array, Bit, NewArray) :-
 
214
        truebit(Array, Bit)
 
215
        ->      NewArray is Array - (1 << Bit)
 
216
        ;       NewArray = Array.
 
217
 
 
218
firstTrue(Array, Begin, Result) :-
 
219
%       (0 is Array >> Begin
 
220
%        -> (write('Error parameter for firstTrue'),
 
221
%               write(Array), writeln(Begin), halt)
 
222
%       ; true),
 
223
        truebit(Array, Begin)
 
224
        ->      Result = Begin
 
225
        ;       (Next is Begin+1,
 
226
                 firstTrue(Array, Next, Result)).
 
227
*}
 
228
%%=============================================================================
 
229
%%      properties
 
230
 
 
231
%% deadlock free
 
232
 
 
233
dlf     -= [-]dlf /\ <->tt.
 
234
 
 
235
% no starvation for NRT traffic
 
236
 
 
237
ns(I)   -=    [{startcycle}]nsY(I)
 
238
           /\ [-]ns(I).
 
239
nsY(I)  -=    [{endcycle}]nsZ(I)
 
240
           /\ [-{nrt(I),endcycle}]nsY(I).
 
241
nsZ(I)  +=    <->tt
 
242
           /\ [-{nrt(I)}]nsZ(I).