This is a *great* question. We have a paper solution, but none that is
currently implemented in BitC.
The issue you raise (assuming that I have understood you properly) isn't
really specific to ring buffers. It actually has two parts:
1. Parameterizing over array sizes
2. Dealing with *dynamically* sized arrays.
The first part is simple: as we introduced the 'nat' kind, arrays will fold
into the language more naturally, and it will be possible to write something
like (don't hold me to syntax here):
struct S('len:nat)
is
len: 'len
a: array(char, 'len)
you can then instantiate S(5) or S(6) or ...
but this is not always a solution to the problem you raise. It supports
genericity over array sizes, but it still requires that the array size be
part of the "type" of the message. This isn't dynamic arrays.
The next move is to combine this with capsules, and region types, which lets
us make types like array-ref more general while encapsulating the concrete
size.
But ultimately, there exist protocols whose lengths are necessary dynamic,
and this pushes us into truly dependent type. For the moment, that's a line
that I still don't feel like I understand adequately, and it's therefore a
line that I don't want to cross in BitC at the moment. My "solution", such
as it is, is to declare somewhat arbitrarily that some kinds of safety
shouldn't be handled within the language, and that message management is one
of those. It's usually a good idea to have an independent specification
language for messages in any case, and where that is true we can rely on
safety mechanisms that are external to the language and perhaps beyond the
checking capabilities of the (current) type system.
Mind you, I think that this is a problem that *desperately* needs a language
solution. All other aspects of safety taken together are insignificant in
comparison to I/O marshalling overheads and the consequent non-locality. On
the face of it, dependent types seem to be required to deal with this. On
the other hand, I/O is something that happens at the "edge" of the runtime
environment, and one may therefore hope that *ad hoc* solutions may hold the
dependent type wolf at bay for some time yet.
In short, I have some sketchy thoughts, but no comprehensive solution. In
the near term, I think that holding the wolf off is both possible and wise.
The next round of type system evolution (coming as soon as we self-host)
should address these issues.
All that having been said, I'ld truly welcome discussions on the subject of
whether we should bite off dependent type in the next round. We're dancing
around the edges already...
shap
On Thu, Oct 28, 2010 at 6:36 PM, Ben Kloosterman <[email protected]> wrote:
> Hi All,
>
> I have a ring buffer that contains variable length messages with a 4 byte
> header ( which contains the size , type and some flags ) followed by 0..n
> caller specified data. Data Alignment may be 4 , 8 , 16 ,32 or 64 bytes
> depending on the buffer ( header alignment is hence 4 bytes) .
>
> The Api is of the form
>
> data_ptr send ( type, size , flags);
> clients then writes a structure to the data pointer possibly using SSE .
>
> OR
>
> void small_send ( type , size , flags , &buffer);
>
> I see there is a word type to hold pointers but don't see any pointer type
> operators such as * and & in the spec did I miss them ?
>
> Is this scheme possible in BitC or is a wrapper around C better ?
>
>
> Ben
>
>
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
