Writing specifications in Sockeye3
==================================

Sockeye3 is a toolchain for specifying and analyzing memory addressing of
hardware platforms.

The Sockeye3 compiler is written in Rust, and features an accompanying
domain-specific language (DSL) for specifying SoCs.

The resulting spec can be fed into the sockeye3 compiler, which can then can
then run queries, generate visualization, and so on.

Checking out the source code
----------------------------

Sockeye3 is `available open-source
<https://gitlab.inf.ethz.ch/project-opensockeye/sockeye3>`__. To check out and
build the sockeye3 tool, simply clone the repository and run `cargo build`::

  git clone https://gitlab.inf.ethz.ch/project-opensockeye/sockeye3
  cd sockeye3
  cargo build # add --release for a release build

Alternatively, Sockeye3 is also distributed as part of the :ref:`Kirsch
toolchain <toolchain-setup>`.

Organization of the source tree
-------------------------------

.. note::
   These instructions were written for sockeye3 commit
   ``9237cca90209cf8bf0d4d2391b5726ecc34c6bb4``.

The Sockeye3 source tree contains the Rust-based compiler. Hardware
specifications are stored in a `separate repository
<https://gitlab.inf.ethz.ch/project-opensockeye/sockeye-specifications>`__,
which is included as a submodule in the subdirectory ``specs/``.
Rust enforces a naming scheme for modules, namely that the file
``src/module.rs`` contains the export definitions for the source files in
``sockeye3::module``. That said, Sockeye3 contains the following modules:

``sockeye3::decoding_net``
  Contains the definitions of a ``DecodingNet``, and basic tools for
  manipulating decoding nets: adding address spaces, mappings, and annotating
  additional information.

``sockeye3::specification``
  Contains the definitions of a ``Specification``, which is a combination of
  individual modules that form the whole decoding net.

``sockeye3::glas``
  Contains code that derives and exports a :ref:`global logical address space
  <glas>` from a Sockeye3 model.

.. _spec organization:

Reading Sockeye specifications
------------------------------

The folder ``specs`` contains all specifications we have written so far. We
organize these specifications roughly by vendor and component.

The specification of a platform can be divided into several (sub-)modules,
which are then assembled in a top-level ``.soc`` file. A SoC-file consists of a
list of imports, instantiations, and connections.

A module is a (potentially) reusable component part of an overall specification.
A module consists of a number of *address spaces*, which are connected by
*mappings*. Together, these form a local decoding net, defining how addresses
are translated locally by this piece of Sockeye.

In order to interface with other modules, these address spaces can be
designated as in- and outports, respectively. An *inport* receives incoming
connections from other modules, while an *outport* provides directed
connections to other modules. Connections between modules are only possible
between an originating outport, and a receiving inport.

Below is a screenshot generated from the specification contained in
``specs/example_vendor/example.soc``. This is a fictional, 2-core system with a
built-in network interface card, intended to show the basic features of our
DSL.

.. figure:: /_static/images/screenshot_nic_module_graphviz.png
   :align: center
   :alt: Screenshot showing the 'nic' module from our fictional example.

   An excerpt of a system specification, showing a Sockeye module for a NIC,
   consisting of separate address spaces for the NIC core, the NIC's registers,
   and a mapped to the main interconnect. Gray arrows denote module-internal
   mappings, while black arrows denote inter-module connections.

The code that defines the NIC module is shown below. The comments give brief
explanations of the individual address spaces and mappings.

.. code-block:: sockeye
   :caption: specs/example_vendor/example/nic.gls

   /// This module describes a fictional network interface card, i.e. a
   /// component that issues memory operations, 
   
   /// This network interface card has a 32-bit physical address space,
   /// therefore we create a 4GiB address space for the execution context.
   ctx nic_core 4GiB
   
   /// Part of this context's address space is mapped to the main interconnect,
   /// therefore we create an appropriate address space here.
   as to_interconnect 4GiB
   out to_interconnect
   
   /// The NIC features 64kiB of registers, accessible via the main
   /// interconnect. Therefore, we mark the registers as an 'in' address space.
   dev registers 64kiB
   in registers
   
   /// The upper 3GiB are mapped to the system interconnect.
   map nic_core @ 0x4000_0000 -> to_interconnect @ 0x4000_0000 (3GiB)
   
   /// The NIC can also access its registers at 0x0.
   map nic_core @ 0x0 -> registers @ 0x0 (64kiB)

The whole system is then described in a top-level ``.soc`` file, shown below.

.. code-block:: sockeye
   :caption: specs/example_vendor/example.soc

   /// We can import modules from arbitrary paths, relative to our .soc file.
   import example/dram.gls
   import example/nic.gls
   import example/core.gls
   import example/interconnect.gls
   
   /// The imported modules can then be instantiated. Each instantiation has
   /// its own address spaces and mappings.
   inst xconn interconnect
   inst dram dram
   inst nic nic
   inst core_0 core
   inst core_1 core
   
   /// The ports of instances can then be connected, forming the full specification.
   conn core_0.core -> xconn.input
   conn core_1.core -> xconn.input
   conn nic.to_interconnect -> xconn.input
   conn xconn.nic_registers -> nic.registers
   conn xconn.dram -> dram.dram

The final specification looks like this:

.. figure:: /_static/images/example_soc.png
   :align: center
   :width: 600

   Visualization of the decoding net generated by ``example.soc``

Writing Sockeye specifications
------------------------------

In order to write a new Sockeye specification, we only need to create a new
top-level ``.soc`` file, and point the ``sockeye3`` tool at it.

.. code-block:: bash

   # Create the new specification file
   touch my_new_spec.soc
   # Run sockeye3
   sockeye3 my_new_spec.soc
   [INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (0 address spaces) [0s]
   [INFO  sockeye3::cli] Successful run, terminating [0s]

This specification is not very interesting yet, since we haven't specified
anything. Let us create a new module now:

.. code-block:: bash

   # Create initial address spaces
   cat <<EOF > my_new_module.mod
   ctx my_context 128kiB
   as my_interconnect 64kiB
   mem my_memory 64kiB
   EOF

This module defines three address spaces, a context of 128 Kibibytes size, an
interconnect of 64 Kibibytes, and finally some memory also 64 Kibibytes in size.
In order for this module to show up in our specification, we need to import and
instantiate it:

.. code-block:: bash

   # Import and instantiate the new module
   cat <<EOF > my_new_spec.soc
   import my_new_module.mod
   inst my_instance my_new_module
   EOF
   # Re-run sockeye3
   sockeye3 my_new_spec.soc
   [INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (3 address spaces) [0s]
   [INFO  sockeye3::cli] Successful run, terminating [0s]

We can visualize these address spaces by outputting a graphviz description.

.. code-block:: bash

   # Generate a graphviz description of the decoding net, and output it to my_viz.dot
   sockeye3 my_new_spec.soc --graphviz my_viz.dot
   [INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (3 address spaces) [0s]
   [INFO  sockeye3::cli] Dot output to my_viz.dot
   [INFO  sockeye3::cli] Successful run, terminating [0s]
   # Compile the resulting description to a PNG image
   dot -Tpng -o my_viz.png < my_viz.dot

.. figure:: /_static/images/my_viz_no_map.png
   :align: center

   The compiled graphviz description from ``my_new_spec.soc``.

Our address spaces show up now, colored in different colors according to their
attribute (context, intermediate, resource). What these attributes mean in
detail will be explained later.

Let us add some mappings to our specification, and see how it changes the
visualization.

.. code-block:: bash

   # Add some mappings
   cat <<EOF >> my_new_module.mod
   map my_context @ 0x0 -> my_interconnect @ 0x0 (64kiB)
   map my_interconnect @ 0x0 -> my_memory @ 0x0 (64kiB)
   EOF
   # Re-run sockeye3
   sockeye3 my_new_spec.soc --graphviz my_viz.dot
   [INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (3 address spaces) [0s]
   [INFO  sockeye3::cli] Dot output to my_viz.dot
   [INFO  sockeye3::cli] Successful run, terminating [0s]
   # And also re-run dot
   dot -Tpng -o my_viz.png < my_viz.dot

.. figure:: /_static/images/my_viz_map.png
   :align: center

   Mappings now show up as arrows between address spaces.

Most systems are more complicated than a single module, however. In our case,
the context has another 64kiB of address space that are not utilized. It turns
out that these are connected to the interconnect of an identical core. In order
to represent this in our model, we add another address space to our module, which
will be connected to the other interconnect.

.. code-block:: bash

   # Add a new address space that maps to the other interconnect, and
   # add the corresponding mapping to the upper 64KiB of my_context.
   cat <<EOF >> my_new_module.mod
   as to_other_interconnect 64KiB
   map my_context @ 64KiB -> to_other_interconnect @ 0x0 (64KiB)
   EOF

This by itself is insufficient, however, as we haven't declared our interconnect
as a valid connection point. Therefore, we additionally have to declare
the address space ``to_other_interconnect`` as valid *outport*, and the address
space ``my_interconnect`` as valid *inport*.

.. code-block:: bash

   # Add the in- and outport declarations
   cat <<EOF >> my_new_module.mod
   out to_other_interconnect
   in my_interconnect
   EOF

Now we can instantiate another module, and connect up the address spaces. Note
that this specification only connects the instances one way, namely from
``my_instance`` to ``other_instance``. If we want the reverse connection to
appear as well, we need another ``conn`` statement.

.. code-block:: bash

   # Create a second instance of my_new_module, and connect the
   # corresponding address spaces.
   cat <<EOF >> my_new_spec.soc
   inst other_instance my_new_module
   conn my_instace.to_other_interconnect -> other_instance.my_interconnect
   # All address spaces show up twice now, once for each instance
   sockeye3 my_new_spec.soc --graphviz my_viz.dot
   [INFO  sockeye3::cli] Parsed specification from my_new_spec.soc (8 address spaces) [0s]
   [INFO  sockeye3::cli] Dot output to my_viz.dot
   [INFO  sockeye3::cli] Successful run, terminating [0s]

.. figure:: /_static/images/my_viz_2.png
   :align: center

   There are multiple instances of ``my_new_module`` now.

Now you know the basics to start specifying your own SoCs. The next section
contains a brief summary of the Sockeye syntax.

The Sockeye syntax
~~~~~~~~~~~~~~~~~~

The code block below shows a brief summary of expressions in sockeye.

.. code-block:: sockeye

   // Comments are written using two slashes, and continue to the end of the line.
   /// Doc-comments use triple slashes.

   ///////////////////////////////////////////////////////////////////////////////
   // A SoC file consists of import, inst, and conn statements.

   // Imports
   // import <path> 
   import some/path/to/some/module.mod

   // Instantiation
   // inst <instance_name> <module_name>
   inst my_instance my_module

   // Connections
   // conn <instance>.<address_space> -> <instance>.<address_space>
   conn inst0.core -> inst1.interconnect

   ///////////////////////////////////////////////////////////////////////////////
   // A module file consists of address space declarations, mappings, and port
   // declarations.

   // Address spaces
   // <address_space_type> <name> <size>

   // Generic address spaces are declared using 'as'
   as generic_address_space 1024B

   // Contexts
   // Things that issue memory requests are declared using 'ctx'.
   ctx context 1KiB
   ctx my_dma_engine 16MiB

   // Resources
   // Things that answer memory requests are declared either to be
   // memory (mem), device registers (dev), or generic/unknown (res).
   res my_generic_resource 3KiB
   mem my_large_dram 5PiB
   dev my_dma_engine_configuration 16KiB

   // Mappings
   // map <source_address_space> @ <offset> -> <target_address_space> @ <offset> (<size>)
   map core @ 0x0 -> interconnect @ 0x0 (4GiB)
   map interconnect @ 0x123_0000 -> dev1 @ 0x0 (16KiB)
   map interconnect @ 0x126_0000 -> dev2 @ 0x0 (16KiB)
   map interconnect @ 0x800_0000 -> ram @ 0x0 (5GiB)
   
   // Ports
   // <port_type> <address_space>

   // Address spaces are declared as ports using 'in' or 'out', depending on
   // the port type.
   out core
   in interconnect
   in dram

Using Sockeye models in practice
--------------------------------

Now that we know how to define Sockeye models, we need to know how to visualize
and use them. The Sockeye toolchain provides a command-line interface for
processing specifications.

The ``--help`` flag prints a list of arguments with their descriptions.

.. code-block:: text

   $ sockeye3 --help
   Usage: sockeye3 [OPTIONS] <SPEC_PATH>
   
   Arguments:
     <SPEC_PATH>
   
   Options:
         --derive-glas                    Derive a global logical address space
         --load-glas <LOAD_GLAS>          Path to deserialize the GLAS from
         --save-glas <FILE>               Path to serialize the GLAS to
         --glas-out <FILE>                Path to output GLAS to
         --glas-constraints <FILE>        Additional constraints for GLAS derivation
         --glas-try-optimal               Attempt to derive an optimal GLAS, minimizing the number of non-zero offsets.
         --glas-format <GLAS_FORMAT>      [possible values: json]
         --matrix-out <MATRIX_OUT>        Path to output the hardware matrix to
         --matrix-format <MATRIX_FORMAT>  [default: text] [possible values: json, text]
         --graphviz <FILE>                File path to output a graphviz visualization to
         --focus <ADDRESS_SPACE>          Address space to focus (e.g. for visualizations)
     -v, --verbose                        Enable verbose output
     -h, --help                           Print help
     -V, --version                        Print version

Generating visualizations
-------------------------

You can output a `graphviz <https://graphviz.org>`__ descriptions of a
specification via the ``--graphviz`` commands. They will output a dot
description of the requested graph to the given path, which can then be further
processed with ``dot``, as we have seen before. Using the ``--focus`` argument,
we can zoom in on a target address space.

This output is useful for getting an overview of the components present on a
given platform, as well as debugging specifications as you write them.

Deriving a Global Logical Address Space
---------------------------------------

The ``--derive-glas`` flag attempts to derive a :ref:`GLAS <glas>` for the
current decoding net. The ``--glas-out`` flag defines where to output the
computed GLAS to. Additionally, a GLAS can be serialized using the
``--save-glas`` flag, which can later be loaded using ``--load-glas``.

Using ``--glas-out``, we can select the output format for the GLAS. The JSON
format suitable for ingestion into e.g. our `patched version of microkit
<https://gitlab.inf.ethz.ch/OU-ROSCOE/sockeye/os4rc/sel4-glas/sel4-microkit>`_.

Sockeye allows the user to specify additional constraints that must be
satisfied of the GLAS. The constraints can be given in two forms::

   ctx_constraint ctx @ local_addr, len -> glas_addr
   res_constraint res @ res_addr, len -> glas_addr

A ``ctx_constraint`` forces the resource that appears at ``local_addr`` of
context ``ctx`` to appear at address ``glas_addr`` in the GLAS. Similarly, a
resource constraint forces the resource to be placed at ``glas_addr`` for *all*
contexts. Note that the latter can easily lead to an unsatisfiable GLAS
configuration, so use it with care.