|
|
@@ -1,8 +1,16 @@
|
|
|
# Gidl
|
|
|
|
|
|
+
|
|
|
+
|
|
|
Gidl (for Galois Interface Description Language) is a simple IDL for
|
|
|
describing structured types and RPC-style interfaces.
|
|
|
|
|
|
+## Overview
|
|
|
+
|
|
|
+[Jump right to an example of gidl.](https://github.com/galoisinc/gidl/tree/master/tests/example.idl)
|
|
|
+
|
|
|
+### Types
|
|
|
+
|
|
|
Gidl has a type language which permits the user to define types using
|
|
|
the following primitives:
|
|
|
- Atomic types:
|
|
|
@@ -20,12 +28,15 @@ the following primitives:
|
|
|
- Set of named fields. Corresponds to a record or a C struct.
|
|
|
- All fields are atomic, enum, or newtypes.
|
|
|
|
|
|
+### Interfaces
|
|
|
+
|
|
|
Gidl interfaces are composed of the following primitives:
|
|
|
-- Streams, which are sent from server to client periodically
|
|
|
+- Streams, which are sent from server to client whenever the server wants.
|
|
|
+ (We expect to refine this and allow clients to control stream rate.)
|
|
|
- Attributes, which are read and written according to requests by the client.
|
|
|
Attributes have a user defined read/writable permissions.
|
|
|
|
|
|
-Interfaces can be composed by subtyping - java style multiple inheritance.
|
|
|
+Interfaces can be composed by subtyping.
|
|
|
(We expect interface composition may change in the future.)
|
|
|
|
|
|
Protocol drift is detected by identifying each stream and attribute message
|
|
|
@@ -33,20 +44,50 @@ on the wire by a hash of its name, its type, and all child types. Therefore
|
|
|
|
|
|
## IDL format
|
|
|
|
|
|
-The gidl IDL uses a s-expression based format.
|
|
|
-
|
|
|
-See example format: `tests/example.idl`
|
|
|
+The gidl IDL uses a s-expression based format. The IDL format currently is
|
|
|
+documented in `tests/example.idl`
|
|
|
|
|
|
## Backends
|
|
|
|
|
|
Gidl currently has backends for:
|
|
|
- - Native Haskell
|
|
|
- - [Ivory][] types, and [Tower][] interfaces
|
|
|
+ - Haskell backend: translates types to algebraic datatypes, creates `cereal`
|
|
|
+ instances for serialization. RPC client layer in progress.
|
|
|
+ - [Ivory][] backend: translates types to Ivory types, creates `ivory-serialize`
|
|
|
+ instances for serialization.
|
|
|
+ - [Tower][] backend: all of the features of the Ivory backend, and also
|
|
|
+ creates datatypes of tower channels for interface streams and attributes,
|
|
|
+ and a tower monitor which implements a server for a given interface.
|
|
|
|
|
|
[Ivory]: http://github.com/GaloisInc/ivory
|
|
|
[Tower]: http://github.com/GaloisInc/tower
|
|
|
|
|
|
+## Prerequisites
|
|
|
+
|
|
|
+Gidl requires the GHC 7.8 haskell compiler, and a modern Cabal (>= 1.18).
|
|
|
+
|
|
|
+It also requires the [`s-cargot`][] package, which is not yet available through
|
|
|
+hackage. In the parent directory, run
|
|
|
+
|
|
|
+```
|
|
|
+git clone https://github.com/aisamanra/s-cargot
|
|
|
+```
|
|
|
+
|
|
|
+[s-cargot]: https://github.com/aisamanra/s-cargot
|
|
|
+
|
|
|
+In order to build the code generated by the the Ivory and Tower backends, we
|
|
|
+require the [Ivory][], [Tower][], and [ivory-tower-stm32][] repositories. These
|
|
|
+should also be found, by default, in the parent directory.
|
|
|
+
|
|
|
+[ivory-tower-stm32]: http://github.com/GaloisInc/ivory-tower-stm32
|
|
|
+
|
|
|
+```
|
|
|
+git clone https://github.com/galoisinc/ivory
|
|
|
+git clone https://github.com/galoisinc/tower
|
|
|
+git clone https://github.com/galoisinc/ivory-tower-stm32
|
|
|
+```
|
|
|
+
|
|
|
## Build and Test
|
|
|
+
|
|
|
Use the `create-sandbox` target in the Makefile to create a local cabal
|
|
|
sandbox and install all dependencies.
|
|
|
|
|
|
@@ -55,4 +96,22 @@ The default target builds the gidl library. You can then use `cabal run gidl --
|
|
|
information.
|
|
|
|
|
|
Use the `test` target in the Makefile to generate and test each backend
|
|
|
-implementation.
|
|
|
+implementation. The `tests/example.idl` file is used as the input language.
|
|
|
+You may then browse generated code for each implementation, which is generated
|
|
|
+and built in subdirectories of the `tests` directory.
|
|
|
+
|
|
|
+## About
|
|
|
+
|
|
|
+Gidl was created at [Galois][] by Pat Hickey, with help from Getty Ritter and
|
|
|
+Trevor Elliott, as part of the [SMACCMPilot project][].
|
|
|
+
|
|
|
+Gidl was inspired in part by John Van Enk's excellent [Cauterize][] tools. Look
|
|
|
+for gidl to switch to using cauterize as the type language in the future!
|
|
|
+
|
|
|
+Gidl is still experimental - anything may change at any time. Please get in
|
|
|
+touch if you're interested in using or working on gidl.
|
|
|
+
|
|
|
+[Galois]: https://galois.com
|
|
|
+[SMACCMPilot project]: https://smaccmpilot.org
|
|
|
+[Cauterize]: https://github.com/cauterize-tools/cauterize
|
|
|
+
|
Pat Hickey