Subversion Repositories tendra.SVN

Rev

Rev 2 | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 7u83 1
<!-- Crown Copyright (c) 1998 -->
2
<HTML>
3
<HEAD>
4
<TITLE>Models of the TDF algebra</TITLE>
5
</HEAD>
6
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" LINK="#0000FF" VLINK="#400080" ALINK="#FF0000">
7
<A NAME=S89>
8
<H1>TDF Guide, Issue 4.0 </H1>
9
<A HREF="guide16.html">
10
<H3>January 1998</H3>
11
<IMG SRC="../images/next.gif" ALT="next section"></A>  
12
<A HREF="guide14.html">
13
<IMG SRC="../images/prev.gif" ALT="previous section"></A>
14
<A HREF="guide1.html"><IMG SRC="../images/top.gif" ALT="current document"></A>
15
<A HREF="../index.html"><IMG SRC="../images/home.gif" ALT="TenDRA home page">
16
</A>
17
<IMG SRC="../images/no_index.gif" ALT="document index"><P>
18
<HR>
19
<DL>
20
<DT><A HREF="#S90"><B>13.1 </B> - Model for a 32-bit standard architecture</A>
21
<DD>
22
<DT><A HREF="#S91"><B>13.1.1 </B> - Alignment model</A><DD>
23
<DT><A HREF="#S92"><B>13.1.2 </B> - Offset and pointer model</A><DD>
24
<DT><A HREF="#S93"><B>13.1.3 </B> - Size model</A><DD>
25
<DT><A HREF="#S94"><B>13.2 </B> - Model for machines like the iAPX-432</A><DD>
26
<DT><A HREF="#S95"><B>13.2.1 </B> - Alignment model</A><DD>
27
<DT><A HREF="#S96"><B>13.2.2 </B> - Offset and pointer model</A><DD>
28
<DT><A HREF="#S97"><B>13.2.3 </B> - Size model</A><DD>
29
<DT><A HREF="#S98"><B>13.2.4 </B> - Offset arithmetic</A><DD>
30
</DL>
31
<HR>
32
<H1>13  <A NAME=0>Models of the TDF algebra</H1>
33
TDF is a multi-sorted abstract algebra. Any implementation of TDF
34
is a model of this algebra, formed by a mapping of the algebra into
35
a concrete machine. An algebraic mapping gives a concrete representation
36
to each of the SORTs in such a way that the representation of any
37
construction of TDF is independent of context; it is a homomorphism.
38
In other words if we define the mapping of a TDF constructor, C, as
39
MAP[C] and the representation of a SORT, S, as REPR[S] then:<P>
40
<PRE>
41
REPR[ C(P<I>1</I> ,..., P<I>n</I>) ] = MAP[C]( REPR(P<I>1</I>) ,..., REPR(P<I>n
42
</I>))
43
</PRE>
44
Any mapping has to preserve the equivalences of the abstract algebra,
45
such as those exemplified by the transformations {A} - {Z} in  
46
<A HREF="guide13.html#4">section 11.1 on page 48</A>. Similarly, the
47
mappings of any predicates on the constructions, such as those giving
48
&quot;well-formed&quot; conditions, must be satisfied in terms of
49
the mapped representations.<P>
50
In common with most homomorphisms, the mappings of constructions can
51
exhibit more equivalences than are given by the abstract algebra.
52
The use of these extra equivalences is the basis of most of the target-dependent
53
optimisations in a TDF translator; it can make use of &quot;idioms&quot;
54
of the target architecture to produce equivalent constructions which
55
may work faster than the &quot;obvious&quot; translation. In addition,
56
we may find that may find that more predicates are satisfied in a
57
mapping than would be in the abstract algebra. A particular concrete
58
mapping might allow more constructions to be well-formed than are
59
permitted in the abstract; a producer can use this fact to target
60
its output to a particular class of architectures. In this case, the
61
producer should produce TDF so that any translator not targeted to
62
this class can fail gracefully.<P>
63
Giving a complete mapping for a particular architecture here is tantamount
64
to writing a complete translator. However, the mappings for the small
65
but important sub-algebra concerned with OFFSETs and ALIGNMENTs illustrates
66
many of the main principles. What follows is two sets of mappings
67
for disparate architectures; the first gives a more or less standard
68
meaning to ALIGNMENTs but the second may be less familiar.<P>
69
<A NAME=S90>
70
<HR><H2>13.1. <A NAME=2>Model for a 32-bit standard architecture</H2>
71
Almost all current architectures use a &quot;flat-store&quot; model
72
of memory. There is no enforced segregation of one kind of data from
73
another - in general, one can access one unit of memory as a linear
74
offset from any other. Here, TDF ALIGNMENTs are a reflection of constraints
75
for the efficient access of different kinds of data objects - usually
76
one finds that 32-bit integers are most efficiently accessed if they
77
start at 32 bit boundaries and so on. <P>
78
<A NAME=S91>
79
<H3>13.1.1. Alignment model</H3>
80
The representation of ALIGNMENT in a typical standard architecture
81
is a single integer where:<P>
82
<PRE>
83
REPR [ { } ] = 1
84
REPR[ {bitfield} ] = 1
85
REPR[ {char_variety} ] = 8
86
REPR[ {short_variety} ] = 16
87
</PRE>
88
Otherwise, for all other primitive ALIGNMENTS a:<P>
89
<PRE>
90
REPR [ {a} ] = 32
91
</PRE>
92
The representation of a compound ALIGNMENT is given by:<P>
93
<PRE>
94
REPR [ A xc8  B ] = Max(REPR[ A ] , REPR[ B ])
95
i.e. MAP[ unite_alignment] = Max
96
</PRE>
97
while the ALIGNMENT inclusion predicate is given by:<P>
98
<PRE>
99
REPR[ A ... B ]= REPR[ A ] xb3  REPR[ B }
100
 
101
</PRE>
102
All the constructions which make ALIGNMENTs are represented here and
103
they will always reduce to an integer known at translate-time. Note
104
that the mappings for xc8  and ... must preserve the basic algebraic
105
properties derived from sets; for example the mapping of xc8  must
106
be idempotent, commutative and associative, which is true for Max.<P>
107
<A NAME=S92>
108
<H3>13.1.2. Offset and pointer model</H3>
109
Most standard architectures use byte addressing; to address bits requires
110
more complication. Hence, a value with SHAPE POINTER(A) where REPR[A)]xb9
111
1 is represented by a 32-bit byte address. <P>
112
We are not allowed to construct pointers where REPR[A] = 1, but we
113
still have offsets whose second alignment is a bitfield. Thus a offsets
114
to bitfield are represented differently to offsets to other alignments:<P>
115
A value with SHAPE OFFSET(A, B) where REPR(B) xb9 1 is represented
116
by a 32-bit byte-offset.<P>
117
A value with SHAPE OFFSET(A, B) where REPR(B) = 1 is represented by
118
a 32-bit <I>bit</I>-offset.<P>
119
<A NAME=S93>
120
<H3>13.1.3. Size model</H3>
121
In principle, the representation of a SHAPE is a pair of an ALIGNMENT
122
and a size, given by shape_offset applied to the SHAPE. This pair
123
is constant which can be evaluated at translate time. The construction,
124
shape_offset(S), has SHAPE OFFSET(alignment(s), { } ) and hence is
125
represented by a bit-offset: <P>
126
<PRE>
127
REPR[ shape_offset(top()) ] = 0
128
REPR[ shape_offset(integer(char_variety)) ] = 8
129
REPR[ shape_offset(integer(short_variety)) ] = 16
130
.... etc. for other numeric varieties
131
REPR[ shape_offset(pointer(A)) ]= 32
132
REPR[ shape_offset(compound(E)) ] = REPR[ E ]
133
REPR[ shape_offset(bitfield(bfvar_bits(b, N))) ] = N
134
REPR[ shape_offset(nof(N, S)) ] = N * REPR[ offset_pad(
135
alignment(S), shape_offset(S)) ]
136
         where S is not a bitfield shape
137
</PRE>
138
Similar considerations apply to the other offset-arithmetic constructors.
139
In general, we have:<P>
140
<PRE>
141
REPR [ offset_zero(A) ] = 0             for all A
142
 
143
REPR[offset_pad(A, X:OFFSET(C,D)) 
144
      		= ((REPR[X] + REPR[A]-1)/(REPR[A]))*REPR[A]/8
145
	if REPR[A] xb9  1 xd9  REPR[D ] =1
146
Otherwise :
147
REPR[offset_pad(A, X:OFFSET(C,D)) 
148
		= ((REPR[X] + REPR[A]-1)/(REPR[A]))*REPR[A]
149
 
150
REPR[ offset_add(X:OFFSET(A,B), Y:OFFSET(C,D) )] 
151
		= REPR[ X ] *8+ REPR[ Y ]
152
        if REPR[B] xb9 1 xd9  REPR[D ] =1
153
 Otherwise:
154
REPR[ offset_add(X, Y )] = REPR[ X ] + REPR[ Y ]
155
 
156
REPR[ offset_max(X: OFFSET(A, B), Y: OFFSET(C, D))]
157
	= Max(REPR[ X ], 8*REPR[ Y ]
158
	if REPR[ B ] = 1 xd9  REPR[D ] xb9  1
159
REPR[ offset_max(X: OFFSET(A, B), Y: OFFSET(C, D))]
160
	= Max(8*REPR[ X ], REPR[ Y ]
161
	if REPR[ D ] = 1 xd9  REPR[ B ] xb9  1
162
Otherwise:
163
REPR[ offset_max(X, Y) ] = Max( REPR[ X ], REPR[ Y ])
164
 
165
REPR[offset_mult(X, E) ] = REPR[ X ] * REPR[ E ]
166
 
167
 
168
</PRE>
169
IA translator working to this model maps ALIGNMENTs into the integers
170
and their inclusion constraints into numerical comparisons. As a result,
171
it will correctly allow many OFFSETs which are disallowed in general;
172
for example, OFFSET({pointer}, {char_variety}) is allowed since REPR[
173
{pointer} ] xb3  REPR[ {char_variety} ]. Rather fewer of these extra
174
relationships are allowed in the next model considered.<P>
175
<A NAME=S94>
176
<HR><H2>13.2. Model for machines like the iAPX-432</H2>
177
The iAPX-432 does not have a linear model of store. The address of
178
a word in store is a pair consisting of a block-address and a displacement
179
within that block. In order to take full advantage of the protection
180
facilities of the machine, block-addresses are strictly segregated
181
from scalar data like integers, floats, displacements etc. There are
182
at least two different kind of blocks, one which can only contain
183
block-addresses and the other which contains only scalar data. There
184
are clearly difficulties here in describing data-structures which
185
contain both pointers and scalar data.<P>
186
Let us assume that the machine has bit-addressing to avoid the bit
187
complications already covered in the first model. Also assume that
188
instruction blocks are just scalar blocks and that block addresses
189
are aligned on 32-bit boundaries.<P>
190
<A NAME=S95>
191
<H3>13.2.1. Alignment model</H3>
192
An ALIGNMENT is represented by a pair consisting of an integer, giving
193
the natural alignments for scalar data, and boolean to indicate the
194
presence of a block-address. Denote this by:<P>
195
<PRE>
196
(s: alignment_of_scalars, b: has_blocks)
197
</PRE>
198
We then have:<P>
199
<PRE>
200
REPR[ alignment({ }) ] = (s: 1, b: FALSE)
201
REPR[ alignment({char_variety}) = (s: 8, b:FALSE)
202
... etc. for other numerical and bitfield varieties.
203
REPR[ alignment({pointer}) ] = (s: 32, b: TRUE)
204
REPR[ alignment({proc}) ] = (s: 32, b: TRUE)
205
REPR[ alignment({local_label_value}) ] = (s: 32, b: TRUE)
206
</PRE>
207
The representation of a compound ALIGNMENT is given by:<P>
208
<PRE>
209
REPR[ A xc8  B ] = (s: Max(REPR[ A ].s, REPR[ B ].s), b: REPR[ A ].b xda  REPR[ B ].b )
210
 
211
</PRE>
212
and their inclusion relationship is given by:<P>
213
<PRE>
214
REPR[ A ... B ] = (REPR[ A ].s xb3  REPR[ B ].s) xd9  (REPR[ A ].b xda  &yuml; REPR[ B ].b)
215
</PRE>
216
<A NAME=S96>
217
<H3>13.2.2. Offset and pointer model</H3>
218
A value with SHAPE POINTER A where &yuml; REPR[ A ].b is represented
219
by a pair consisting of a block-address of a scalar block and an integer
220
bit-displacement within that block. Denote this by:<P>
221
<PRE>
222
(sb: scalar_block_address, sd: bit_displacement)
223
</PRE>
224
A value with SHAPE POINTER A where REPR[ A ].b is represented by a
225
quad word consisting of two block-addresses and two bit-displacements
226
within these blocks. One of these block addresses will contain the
227
scalar information pointed at by one of the bit-displacements; similarly,
228
the other pair will point at the block addresses in the data are held.
229
Denote this by:<P>
230
<PRE>
231
(sb: scalar_block_address, ab: address_block_address,
232
  sd: scalar_displacement, ad: address_displacement )
233
</PRE>
234
<P>
235
A value with SHAPE OFFSET(A, B) where &yuml; REPR[ A ].b is represented
236
by an integer bit-displacement.<P>
237
A value with SHAPE OFFSET(A, B) where REPR[ A ].b is represented by
238
a pair of bit-displacements, one relative to a scalar-block and the
239
other to an address-block. Denote this by:<P>
240
<PRE>
241
( sd: scalar_displacement, ad: address_displacement )
242
</PRE>
243
<A NAME=S97>
244
<H3>13.2.3. Size model</H3>
245
The sizes given by shape_offset are now:<P>
246
<PRE>
247
REPR[shape_offset(integer(char_variety)) ] = 8
248
... etc. for other numerical and bitfield varieties.
249
REPR[ shape_offset(pointer(A)) ] = ( REPR[ A ].b ) ? (sd: 64, ad: 64) : (sd: 32, ad: 32)
250
REPR[ shape_offset(offset(A, B)) ] = (REPR[ A ].b) ? 64 : 32)
251
REPR[ shape_offset(proc) ] = (sd: 32, ad: 32)
252
REPR[ shape_offset(compound(E)) ] = REPR[ E ]
253
REPR[ shape_offset(nof(N, S)) ] 
254
                         = N* REPR[ offset_pad(alignment(S)), shape_offset(S)) ]
255
REPR[ shape_offset(top) ] = 0
256
</PRE>
257
<A NAME=S98>
258
<H3>13.2.4. Offset arithmetic</H3>
259
The other OFFSET constructors are given by:<P>
260
<PRE>
261
REPR[ offset_zero(A) ] = 0		                          if  &yuml; REPR[ A ].b
262
REPR[ offset_zero(A) ] = (sd: 0, ad: 0)        		if REPR[ A ].b
263
 
264
REPR[ offset_add(X: OFFSET(A,B), Y: OFFSET(C, D)) ] = REPR[ X ] + REPR[ Y ]
265
	if &yuml; REPR[ A ].b xd9  &yuml; REPR[ C ].b
266
REPR[ offset_add(X: OFFSET(A,B), Y: OFFSET(C, D)) ]
267
                       = ( sd: REPR[ X ].sd + REPR[ Y ].sd, ad: REPR[ X ].ad + REPR[ Y ].ad)
268
	if REPR[ A ].b xd9  REPR[ C ].b
269
REPR[ offset_add(X: OFFSET(A,B), Y: OFFSET(C, D)) ]
270
                       = ( sd: REPR[ X ].sd + REPR[ Y ], ad:REPR[ X ].ad )
271
	if REPR[ A ].b xd9  &yuml; REPR[ C ].b
272
 
273
REPR[ offset_pad(A, Y: OFFSET(C, D)) ] = (REPR[Y ] + REPR[A ].s - 1)/REPR[ A ].s
274
	if &yuml; REPR[ A ].b xd9  &yuml; REPR[ C ].b
275
REPR[ offset_pad(A, Y: OFFSET(C, D)) ]
276
                       = ( sd: (REPR[Y ] + REPR[A ].s - 1)/REPR[ A ].s, ad: REPR[ Y ].ad)
277
	if REPR[ C ].b
278
REPR[ offset_pad(A, Y: OFFSET(C, D)) ]
279
                       = ( sd: (REPR[Y]+REPR[A].s-1)/REPR[A].s, ad: 0)
280
	if REPR[ A ].b xd9  &yuml; REPR[ C ].b
281
REPR[ offset_max(X: OFFSET(A,B), Y: OFFSET(C, D)) ] 
282
                        = Max(REPR[ X ], REPR[ Y ])
283
	if &yuml; REPR[ A ].b xd9  &yuml; REPR[ C ].b
284
REPR[ offset_max(X: OFFSET(A,B), Y: OFFSET(C, D)) ]
285
                       = ( sd: Max(REPR[ X ].sd, REPR[ Y ].sd), 
286
                             ad: Max(REPR[ X ].a, REPR[ Y ].ad) )
287
	if REPR[ A ].b xd9  REPR[ C ].b
288
REPR[ offset_max(X: OFFSET(A,B), Y: OFFSET(C, D)) ]
289
                       = ( sd: Max(REPR[ X ].sd, REPR[ Y ]), ad:REPR[ X ].ad )
290
	if REPR[ A ].b xd9  &yuml; REPR[ C ].b
291
REPR[ offset_max(X: OFFSET(A,B), Y: OFFSET(C, D)) ]
292
                       = ( sd: Max(REPR[Y ].sd, REPR[ X]), ad: REPR[Y ].ad )
293
	if REPR[C ].b xd9  &yuml; REPR[ A ].b
294
 
295
REPR[ offset_subtract(X: OFFSET(A,B), Y: OFFSET(C, D)) ] 
296
                       = REPR[ X ]- REPR[ Y ]
297
	if &yuml; REPR[ A ].b xd9  &yuml; REPR[ C ].b
298
REPR[ offset_subtract(X: OFFSET(A,B), Y: OFFSET(C, D)) ]
299
                       = ( sd: REPR[ X ].sd - REPR[ Y ].sd, ad:REPR[ X ].ad - REPR[ Y ].ad)
300
	if REPR[ A ].b xd9  REPR[ C ].b
301
REPR[ offset_add(X: OFFSET(A,B), Y: OFFSET(C, D)) ]
302
                       = REPR[ X ].sd - REPR[ Y ]
303
	if REPR[ A ].b xd9  &yuml; REPR[ C ].b
304
.... and so on.
305
</PRE>
306
<P>
307
Unlike the previous one, this model of ALIGNMENTs would reject OFFSETs
308
such as OFFSET({long_variety}, {pointer}) but not OFFSET( {pointer},
309
{long_variety}) since:<P>
310
<PRE>
311
 REPR [ {long_variety} ... {pointer} ] = FALSE
312
but:
313
 REPR [ {pointer} ... {long_variety} ] = TRUE
314
 
315
</PRE>
316
This just reflects the fact that there is no way that one can extract
317
a block-address necessary for a pointer from a scalar-block, but since
318
the representation of a pointer includes a scalar displacement, one
319
can always retrieve a scalar from a pointer to a pointer.<P>
320
<HR>
321
<P><I>Part of the <A HREF="../index.html">TenDRA Web</A>.<BR>Crown
322
Copyright &copy; 1998.</I></P>
323
</BODY>
324
</HTML>