[<<][staapl][>>][..]

Sat Mar 13 09:04:52 CET 2010

Composing partial state maps

I need to get this going..  Let's look at the assembler typing/sim
stuff, either in staged Scheme or in Haskell.

First point is the datasheet[1].  Let's use the 12F675 since the
instruction set is simpler than the 18F series.

What are the high-level problems?

    * Functional dependencies.  This is easy:

         ADDLW k

         input constraint: 0 <= k <= 255
         function:         (W) <- (W) + k
         status function:  C, DC, Z

      This needs a low-level logic language to express the
      semantics. I.e. at the bottom this should be logic gates, but
      certain compositions should be acellerated by "simulator
      macros".

      The status functions need to be made explicit, so the function
      type is:

           k -> W -> (W,C,DC,Z)

    * Composition / dependency analysis.

      The interesting problem is how to take descriptions that map
      partial state to partial state, and lift them to complete state
      maps so they can be composed and then possibly re-embedded in a
      minimal representation for dependency or "clobber" analysis.


What are the low-level problems?

1. The basic level is logic gates: the bottom line of semantics should
   be as simple as possible.

2. Solve composition of logic gates by dependency analysis.

3. Solve the mapping (simulation) problem, i.e. implement certain
   networks by operations present in an implemented target, which
   could be a high level language, a real machine, an FPGA circuit
   (build accelerated compiler verifiers on FPGA!), ...


What is the essential idea?

  I'm dealing with information on at least 2 levels: network
  connectivity (meta-lang) and network function (object-lang).

  I.e. staging is essential: There are going to be computations on the
  meta-lang (figuring out dependencies, lifting dependencies to
  provide composition).

  How this is implemented doesn't really matter much (Scheme, Haskell,
  MetaOCaml).

   * Scheme: highest flexibility (hackability due to more operational
     nature: just do it) and very simple staging (macros & modules).

   * MetaOCaml: typed staging, might be useful for figuring out static
     structure of the program itself better.

   * Haskell: very flexible type system, but type-level computations
     are somewhat complex.


Functions and resources.

   1. FUNCTIONS: object language: functional dependencies
      (AND,OR,NOT,compositions) between nodes.

   2. RESOURCES: meta language / type system: _physical_
      instantiations of functional networks connecting shared nodes.


Tagless interpreters[2] and embedding of staging in non-staged
languages[3] are going to be essential components to provide insights.

Hardware languages are about instantiation of macros.  Is it possible
to use the ideas behind Ziggurat[4] to provide higher level semantics
of compositions?  I.e. it's simple to pool together a huge number of
gates into an abstraction, and simulate it by simulating the instance
directly.  What is interesting though is to abstract it n the
meta-level (semantics!) not just the human-modular level.

What I mean is: composition of modules in hardware description
languages is about abstraction for the engineer: the engineer has a
(fuzzy) model about how something works and can use this to "proove"
correctness of compositions.  Can this be made more formal?  Can we
use the specification (simplification) as a type of a hardware module?
I.e. how to relate low-level properties/semantics to high-level[3].



The real problem seems to be management of state (resource).  I.e. an
I2C interface isn't a function, it's a state machine.

Anyways.. There's something to learn here.


[1] http://ww1.microchip.com/downloads/en/DeviceDoc/80125H.pdf
[2] http://okmij.org/ftp/tagless-final/APLAS.pdf
[3] http://okmij.org/ftp/Computation/staging/metafx.pdf
[4] http://lambda-the-ultimate.org/node/3179

[Reply][About]

[<<][staapl][>>][..]