Announcing Potential: x86-64 assembler as a Haskell EDSL

Over the years there have been many projects which seek to use advanced types to provide better static-guarantees in low level languages. There are many examples of this in the literature; here are just a few:

  • Cyclone, perhaps the most-cited example of using types to protect memory in low-level settings.
  • Habit, a proposed Haskell dialect which uses a viable form of dependent types to model low-level data structures and their memory management which I recently learned about on reddit, coincidentally in a comment on an earlier post of mine.
  • Some work due to Oleg Kiselyov and Chung-chieh Shan showing that Haskell is a viable setting for embedding a low-level language.

(If you know of others, put them in the comments!)

In December of 2009 I became interested in typed assembly languages and began working on my own, quickly deciding to embed the language into Haskell. At present there are many facets of the language which work well, but there is still a good deal of work to be done.

When I started this, I was unaware of much of the work that had already been done in this direction (I especially wish I had been aware of the Kiselyov-Shan proof of concept). In the course of the project, I’ve learned a bunch of great tricks, and also have learned of a good deal of excellent work done by others that I hadn’t seen promoted elsewhere. Over the next few posts, my goals are threefold:

  • To describe my own project: where it is, what the challenges have been, where I hope for it to go. And to release some source (on github), such as it is.
  • To describe some of the general lessons I’ve learned working on an EDSL in Haskell, to evangelize this approach to problem solving, and to describe some caveats to conventional Haskell wisdom in this setting.
  • To promote some of the work others have done in this area, in the aim of showing just how far along this idea is.

The Potential programming language

Potential is an adaptation of x86-64 assembly language as a domain specific language, embedded in Haskell. It’s ultimate purpose is to provide a setting in which to implement a practical operating system kernel (the next iteration of the Kinetic project). The basic idea is pretty simple:

  • Functions are written in Haskell which more or less correspond to many of the mnemonics in assembly language.
  • The functions carry type signatures which encode the effect that the mnemonic has on machine state, in the form of an indexed (or parametrized) monad.
  • These functions can be composed to form blocks of code. Haskell type inference can be used to determine the assumptions the code blocks make, as well as the condition they leave the machine in upon return.
  • When these functions are executed, they output abstract syntax for x86-64 assembly, which can then be pretty-printed to a .asm file, which is then passed onto a toolchain for actually compiling the code.

Potential provides the following:

  • An ability to safely handle bit-fields. Bit fields can be defined using Template Haskell, which will automatically generate code for getting and setting elements of the bit field. Potential uses type-level integers to keep track of the sizes of fields, thereby providing a static guarantee that data isn’t getting truncated along the way. (This idea has also been proposed independently in Habit). Potential is able to use this static data to compute the shifts and bit masks necessary for updating and using bit fields.
  • Higher data structures (those built out of bit-fields) are commonplace in the x86-64 standard, and Potential provides a syntax for assembling these as well. Syntax is also provided for defining arrays of such structures, as is needed (for instance) in defining the interrupt descriptor table.
  • A form of linear types, inspired directly by Kiselyov and Shan’s Lightweight monadic regions, for managing pointers.
  • Overloaded >>, >>=, and return operators for use with do notation, allowing programmers to write their assembler in Haskell’s imperative syntax.
  • Predefined versions of the important x86-64 data structures, as well as instructions for making type-level assertions about the state of the hardware. (For instance: are interrupts disabled? Is paging enabled? Is the current privilege level Kernel mode?)
  • Type-level, static tracking of many assembly language subtleties. For instance, the assembly comparison mnemonic (cmp) releases a variable to the programmer which is then passed to the conditional mnemonics (such as je) as a way of demonstrating that the correct comparison is being examined. As an example, the code sequence

    compare1 <- cmp rax rbx
    compare2 <- cmp r09 r10
    sje <some function> compare1
    

    fails to type check because Potential knows that the result of the comparison labeled by compare1 is no longer stored in the CPU’s flags register. As more of assembly gets introduced into Potential, there will be more examples of this type of subtlety being brought directly to the programmer’s eyes, all modeled by types.

  • Every good assembly language needs a good macro language to scrap boiler plate. In the case of Potential, all of Haskell is available as the macro language.
  • Since the language is embedded in Haskell, the result is an assembly language which is essentially as polymorphic as Haskell is, including support for Haskell type class machinery.

All of the above is (at least partially) implemented today. The next major step (according to the plan) is to expand the the memory system so that it can deal with the complexities of paged memory.

Here are just a few of the simple things that are (in some cases, should be) possible in Potential:

  • Code which must execute with interrupts disabled can assert this requirement on the level of types; Haskell will verify that no function invokes such code without first disabling interrupts.
  • The processor flag which enables paged memory cannot be enabled unless the current interrupt descriptor table has a present vector for handling page faults.
  • The task-switching interrupt handler can assert that processor state is preserved between task changes.
  • If two registers carry pointers to the same address, and one of the pointers is used to modify a data structure in a way which modifies its type, the other pointer is implicitly invalidated, and subsequent attempts to use it will result in an error detected by the Haskell type system.

The language is very much still a work in progress with large amounts of rework taking place every few days (owing to the complexity of getting the types to line up with expectations and getting them to be inferred with the appropriate balance of generality and specificity).

Some examples of code written in Potential

Let’s look at some code which is used to modify an interrupt gate. Interrupt gates are used in x86-64 to describe interrupt handlers to the CPU. Structurally, they consist of a small number of bitfields which are used to indicate things like the privilege level that the interrupt handler should execute as (called the “descriptor privilege level,” or DPL). We’ll look at this particular field in these examples.

In Potential, the interrupt gate data structure is defined like so:

intGate = mkStruct "InterruptGate"
                   [ (field 16 "offset_lo")
                   , (field 16 "segsel")
                   , (field 3 "ist")
                   , ($(constField 2) CB0 CB0)
                   , ($(constField 3) CB0 CB0 CB0)
                   , ($(constField 4) CB1 CB1 CB1 CB0)  -- defines Interrupt Gate type
                   , ($(constField 1) CB0)
                   , (field 2  "dpl")
                   , (field 1  "p")
                   , (field 16 "offset_mid")
                   , (field 32 "offset_hi")
                   , ($(reservedField 32))
                   ]

We see the use of some Template Haskell as a matter of convenience (to allow for the constField variadic function). This defines various named fields that can be modified at run-time, as well as some constant fields, and some areas which are reserved for future changes to the x86-64 platform. As is the rule with Template Haskell, this code resides in a module (IntGateStruct) which is, in turn, loaded by another module (IntGate) that reifies it.

Once the IntGate module reifies the structure, Template Haskell is used to define a sequence of new types and top level definitions that can be used to modify InterruptGate structures. It introduces a new InterruptGate type:

> :info InterruptGate
newtype InterruptGate offset_lo segsel ist dpl p offset_mid offset_hi
  = InterruptGate (offset_lo,
                   segsel,
                   ist,
                   dpl,
                   p,
                   offset_mid,
                   offset_hi)
  	-- Defined at Potential/Machine/IntGate.hs:26:0-19

and provides us with some tools we can use to modify such types.

The setField instruction, for instance, is an example of a Haskell-built macro in Potential that can be used to update fields within such structures. Using it, we’re able to write a function that can be used to update the DPL of an interrupt gate:

-- rax contains Ptr64 to interrupt gate
-- rbx contains the new DPL
setDPL = asCode "setDPL" $
     do push rcx
        push rbx
        setField dpl rax rbx rcx
        pop rbx
        pop rcx
        ret

Here some (Haskell) code comments document that rax is used to pass in pointer to the interrupt gate we want to update, and rbx contains the new value for the DPL. The setField macro also needs a register to temporarily use: in this case, we’ve chosen rcx, whose value we are preserving by using the stack (the macro will also modify rbx, so we’re using the stack to preserve that value as well).

We can then ask Potential to translate this code into AT&T-syntax assembler (of course, we could modify the pretty-printing to use a different syntax). Here’s the result of that output (presuming I haven’t many any silly errors in the printer, this should be the right sequence of instructions for performing this operation — if you notice anything to the contrary, let me know!)

> renderFn setDPL 
setDPL:
    push %rcx
    push %rbx
    // updating field "dpl" at (%rax) using value in %rbx, with %rcx as a temp register
    mov 0(%rax) %rcx
    shl 45 %rbx
    and 0xffff9fffffffffff %rcx
    or %rbx %rcx
    mov %rcx 0(%rax)
    // update complete
    pop %rbx
    pop %rcx
    ret

But what about types? Even though we haven’t given a type signature for setDPL, Haskell is (of course) able to infer one for us. We can inspect the type using the Potential function getType.

We can inspect the type of setDPL, as shown below. To make things manageable, I’ve elided much of the class-related output. You can see how type-level integers are used to encode assumptions about the side of arguments, in this case verifying that the arguments are (1) appropriately sized to be pushed onto the stack, and (2) appropriately sized to fill in the DPL field in the interrupt gate:

> :t getType setDPL 
getType setDPL
  :: (SZ rcx
      :<= S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
      SZ rbx
      :<= S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
      SZ rbx :== S (S Z)) =>
     Function
       ConstraintsOn
       (MS
          (Ptr64
             h1
             (InterruptGate offset_lo segsel ist base p offset_mid offset_hi))
          rbx
          rcx
          rdx
          rsi
          rdi
          rbp
          (Ptr64 h (Stack (Ptr64 h11 b11) (Stack a' b')))
          rflags
          rip
          r08
          r09
          r10
          r11
          r12
          r13
          r14
          r15
          (Allocator hn hs cs)
          cmp)
       (MS
          (Ptr64
             (HS (HS hn))
             (InterruptGate offset_lo segsel ist rbx p offset_mid offset_hi))
          rbx
          rcx
          rdx
          rsi
          rdi
          rbp
          (Ptr64 b3 (Stack a' b'))
          rflags
          rip
          r08
          r09
          r10
          r11
          r12
          r13
          r14
          r15
          (Allocator
             (HS (HS (HS (HS (HS (HS hn))))))
             (C (HS (HS (HS (HS (HS hn))))) hs'5)
             (C b2 (C b1 (C h2 (C h1 (C b (C h cs)))))))
          cmp)

Notice that the Ptr64 type carries two things: the first is a handle, in the style of Kiselyov and Shan’s Lightweight monadic regions, and the second is the type of the data being pointed to.

As pointers are manipulated, the handles are closed and new ones issued, in order to statically prevent pointer aliasing from undermining type safety. As we see in this example, the handle for our interrupt gate pointer has changed from h1 to (HS (HS hn)). We can also see that, in the process, the h1 handle is removed from the list of open handles (the third field in the Allocator type records handles which have been closed).

Here is a typical example of why this is necessary: rax points to an interrupt gate whose DPL is set to User. After mov rax rbx, rbx now aliases this pointer. If we then update the DPL field via the rax pointer, we run into a situation where rax and rbx carry the same address but give it different types!

To get around this, whenever a structure manipulated in a way that changes its type, the pointer is modified to keep up: its handle (just prior to update) is closed and replaced with a new handle, reflecting the change. Any aliases of the pointer (prior to update) are now invalid, as tracked by the Haskell type system.

In fact, such trouble is indeed caught and detected by getType. Here we see the code for a function which does exactly what I described in this example: it aliases a pointer to an interrupt gate, then attempts to modify both pointers to wind up with an inconsistent DPL in the type. The code for this function:

testSetDPL2 = asCode "testSetDPL2" $
     do assumeType rbx (undefined :: PrivLevelUser)
        mov rax r10
        scall setDPL
        comment "Now rax has PrivLevelUser, r10 has unknown dpl"
        swap rax r10
        comment "Now rax has unknown dpl, r10 has PrivLevelUser"
        pop rbx
        assumeType rbx (undefined :: PrivLevelKernel)
        scall setDPL
        comment "Now rax has PrivLevelKernel, r10 has PrivLevelUser, but it's the same ptr"
        ret

The code will render (at present, the render function doesn’t verify types — only getType does this), and if we render it, we get the following (AT&T) assembly:

> renderFn testSetDPL2
testSetDPL2:
    mov %rax %r10
    call setDPL
    // Now rax has PrivLevelUser, r10 has unknown dpl
    // swapping %rax with %r10
    push %rax
    mov %r10 %rax
    pop %r10
    // swap complete
    // Now rax has unknown dpl, r10 has PrivLevelUser
    pop %rbx
    call setDPL
    // Now rax has PrivLevelKernel, r10 has PrivLevelUser, but it's the same ptr
    ret

However, once we try to inspect the type, we get the following:

> :t getType testSetDPL2

Top level:
    Couldn't match expected type `Potential.Handles.False'
           against inferred type `Potential.Handles.True'
    When using functional dependencies to combine
      Potential.Handles.LOr
        n1 Potential.Handles.True Potential.Handles.True,
        arising from the dependency `n1 n2 -> t'
        in the instance declaration at Potential/Handles.hs:101:9
      Potential.Handles.LOr
        t Potential.Handles.True Potential.Handles.False,
        arising from a use of `testSetDPL2' at :1:8-18

(Of course, ghci isn’t giving us very useful information about why the failure happened; more work is definitely needed in this area. I expect that type families could be used to replace my functional dependencies, and would give much more meaningful errors, but I believe this will require equality constraints in superclasses, which is why I haven’t yet gone down that road.)

Although it is not currently implemented, it should be possible (once a memory allocator is written) to extend this system to also ensure that memory is freed at appropriate times. For instance, when writing the task manager for an operating system kernel, one will need to allocate memory as tasks are spawned. It should be possible to extend the handle system to track when memory is allocated for a particular task, so that when that task exits, it can be ensured that all associated memory is freed. I’m unaware of any trick in C or C++ that would allow such a guarantee to be made.

Here is another example. In this example, test2 is just a simple function whose behavior is immaterial — it just provides a place that we can conditionally jump to.

Consider the code

test11 = asCode "test11" $
     do pop rax
        pop rbx
        pop rcx
        rabxCmp <- cmp rax rbx
        racxCmp <- cmp rax rcx
        sje test2 racxCmp
        ret

We see two comparisons being performed. The latter comparison is used to conditionally jump to test2. If we inspect the type of test11, we get what we’d expect (again we elide much of the class constraint output for the sake of brevity):

> :t getType test11
getType test11
  :: Function
       ConstraintsOn
       (MS
          rax
          rbx
          rcx
          rdx
          rsi
          rdi
          rbp
          (Ptr64
             h
             (Stack
                Int64
                (Stack
                   Int64
                   (Stack
                      Int64
                      (Stack (Ptr64 h11 b11) (Stack (Ptr64 h12 b12) (Stack a' b')))))))
          (FlagsRegister cf pf af zf sf tf if df of' iopl rf ac vif vip id)
          rip
          r08
          r09
          r10
          r11
          r12
          r13
          r14
          r15
          (Allocator hn hs cs)
          cmp)
       (MS
          Int64
          Int64
          Int64
          rdx
          rsi
          rdi
          rbp
          (Ptr64 b5 (Stack a' b'))
          (FlagsRegister
             (CF (CS (CS cmp)))
             (PF (CS (CS cmp)))
             (AF (CS (CS cmp)))
             (ZF (CS (CS cmp)))
             (SF (CS (CS cmp)))
             tf
             if
             df
             (OF (CS (CS cmp)))
             iopl
             rf
             ac
             vif
             vip
             id)
          rip
          r08
          r09
          r10
          r11
          r12
          r13
          r14
          r15
          (Allocator
             (HS (HS (HS (HS (HS (HS (HS (HS hn))))))))
             (C (HS (HS (HS (HS (HS (HS (HS hn))))))) hs'6)
             (C b4 (C b3 (C b2 (C h1 (C b1 (C b (C h cs))))))))
          (CS (CS cmp)))

The very last line indicates that two comparisons have been performed in this block.

Now suppose we modify the function to introduce a bug:

test11 = asCode "test11" $
     do pop rax
        pop rbx
        pop rcx
        rabxCmp <- cmp rax rbx
        racxCmp <- cmp rax rcx
        sje test2 rabxCmp
        ret

The change is subtle — here we are now attempting to conditionally jump on rabxCmp, which is a comparison whose results should no longer be held in the flags register. Indeed, Potential catches this bug when we attempt to load the code in ghci:

TestCode.hs:54:1:
    Occurs check: cannot construct the infinite type: cmp1 = CS cmp1
      Expected type: PState
                       Instr
                       c
                       (Potential.MachineState.Set
                          Potential.MachineState.RRflags
                          (FlagsRegister
                             (CF (CS (CS cmp1)))
                             (PF (CS (CS cmp1)))
                             (AF (CS (CS cmp1)))
                             (ZF (CS (CS cmp1)))
                             (SF (CS (CS cmp1)))
                             tf
                             if'
                             df
                             (OF (CS (CS cmp1)))
                             iopl
                             rf
                             ac
                             vif
                             vip
                             id)
                          rax
                          rbx
                          rcx
                          rdx
                          rsi
                          rdi
                          rbp
                          (Ptr64 h (Stack (Ptr64 h1 b1) (Stack a' b')))
                          (FlagsRegister
                             (CF (CS cmp1))
                             (PF (CS cmp1))
                             (AF (CS cmp1))
                             (ZF (CS cmp1))
                             (SF (CS cmp1))
                             tf
                             if'
                             df
                             (OF (CS cmp1))
                             iopl
                             rf
                             ac
                             vif
                             vip
                             id)
                          rip1
                          r081
                          r091
                          r101
                          r111
                          r121
                          r131
                          r141
                          r151
                          alloc
                          (CS (CS cmp1)))
                       y
                       a
      Inferred type: PState
                       Instr
                       c
                       (MS
                          rax
                          rbx
                          rcx
                          rdx
                          rsi
                          rdi
                          rbp
                          (Ptr64 h (Stack (Ptr64 h1 b1) (Stack a' b')))
                          (FlagsRegister
                             (CF (CS (CS cmp1)))
                             (PF (CS (CS cmp1)))
                             (AF (CS (CS cmp1)))
                             (ZF (CS cmp1))
                             sf
                             tf1
                             if
                             df1
                             of
                             iopl1
                             rf1
                             ac1
                             vif1
                             vip1
                             id1)
                          rip
                          r08
                          r09
                          r10
                          r11
                          r12
                          r13
                          r14
                          r15
                          (Allocator hn hs cs)
                          cmp)
                       (MS
                          rax
                          rbx
                          rcx
                          rdx
                          rsi
                          rdi
                          rbp
                          (Ptr64 b (Stack a' b'))
                          (FlagsRegister
                             (CF (CS (CS cmp1)))
                             (PF (CS (CS cmp1)))
                             (AF (CS (CS cmp1)))
                             (ZF (CS cmp1))
                             sf
                             tf1
                             if
                             df1
                             of
                             iopl1
                             rf1
                             ac1
                             vif1
                             vip1
                             id1)
                          rip
                          r08
                          r09
                          r10
                          r11
                          r12
                          r13
                          r14
                          r15
                          (Allocator (HS (HS (HS (HS hn)))) hs'1 cs')
                          cmp)
                       ()
    In a stmt of a 'do' expression: sje test2 rabxCmp
    In the second argument of `($)', namely
        `do { pop rax;
              pop rbx;
              pop rcx;
              rabxCmp <- cmp rax rbx;
              .... }'

There’s a lot of output, but towards the bottom we see that ghci correctly points to sje test2 rabxCmp as the source of the trouble.

Source preview

At present time, nothing in Potential is being taken as “stable,” so the code is not available on Hackage. However, the project is on github at Potential. The code as of this blog post is in the initial-blog-announce branch.

Basic usage is pretty simple. To play around a bit, get started like so:

$ ghci -fcontext-stack=160 TestCode.hs
*TestCode> renderFn test1
test1:
    pop %rax
    pop %rbx
    pop %rbx
    // swapping %rax with %rbx
    push %rax
    mov %rbx %rax
    pop %rbx
    // swap complete
    ret

(The large context stack is there for the type-level integers.)

Since Potential makes heavy use of optional class constraints, the best way to inspect the type of a function is with :t getType <function name goes here>.

What’s next (Potential-wise)

The system that tracks pointers is still being adjusted. It seems to be doing its job, but it can undoubtedly be improved in terms of producing good human-readable output via getType. Ultimately I’d like to move the system away from functional dependencies, but without equality constraints in superclasses, the illegality of incoherent instances for associated types seems to make this infeasible.

There’s also a good deal of basic assembly that isn’t present in the language right now. jmp can be invoked on top-level defined functions (it’s name in Potential is sjmp for “static jump”), but is not currently implemented for non-literals (that is, jmp rax isn’t implemented).

The only conditional jump instruction in the current source is sje, which permits conditional jumps on equality to a top-level-defined function. At present it is just a hack — type inference with this instruction isn’t quite correct. (This problem relates to verifying that the instructions following the sje mnemonic are typed the same as the code which might be jumped to. This condition, currently missing, is essentially the same as the condition in Haskell that the then and else blocks in an if statement must have the same type.)

For me, the biggest question is one of scale: while Potential seems capable at managing my small examples, will it be practical to write an operating system in this language? Will Potential’s promises of static checking via types deliver? I believe it might, but this issue is far from settled.

What’s next (blog-wise)

In the days to come, I will give some more examples of code written in Potential, as well as some downloads that can be played with. I’ll also dig into some of the issues that have come up during the design and implementation of the language, much in the style of my posts on optional class constraints and polymorphic first-class labels, which both arose during this project. I’ll also describe some related work that has really come in to save my skin design-wise.

About these ads
Leave a comment

14 Comments

  1. Very interesting work! A couple questions:

    * Why x86-64
    * Have you read Ohori’s “A proof theory for machine code”? I want to apply it to proving assembly-level programs safe, you may find it interesting.
    * Did you take any inspiration from the Harpy project?

  2. * x86-64 mostly satisfies the goal of providing a language I can write a kernel in (besides the necessary step of getting the machine into 64-bit mode, a problem I’m currently relegating to a boot loader).

    Of course, there’s no reason extra state couldn’t be added to Potential to track which mode the CPU is in, allowing for the possibility of supporting full x86 assembly (all modes), and indeed, this would be a logical change for the future.

    * I haven’t read the Ohori paper, but certainly will this weekend!

    * Harpy and ATS join the list of things I wish I had seen sooner. They both look fascinating.

    Harpy raises many interesting questions: should I be using the FFI libraries to describe low-level data structures? Should I adapt Potential to make use of Harpy? This could be a very strong move for Potential.

    Edit: links to Harpy and the Atsushi Ohori paper.

  3. 1. Will full x86-64 assembly be supported? Or at least basic primitives (for example lock cmpxchg to implement spinlock for example)?
    2. Is only writing assambly supported (no ‘inline support’)?

  4. The language’s goal is to provide a solid foundation for the development of a useful (multi-tasked, multi-processor, etc) microkernel, so certainly the basic primitives will be there. I don’t currently have plans to implement the more specialized instructions (such as those that are useful for, say, numerical work), although the machine hardware that supports these instructions will be added to the language model (so that the compiler can verify that task switching correctly preserves the state of these registers).

    Potential is used to output assembly, but not to inline it into Haskell. As far as I can tell, safely inlining assembly into Haskell would require a language model that was intimately familiar with how the run time system operates, or alternatively, would require the compiler to be aware of the types of conflicts that may arise (the latter is the case with inlined assembly in C, for instance).

    Harpy provides a service which is similar to inlined assembly, though: one can define functions which are written in assembly and integrated into Haskell programs via the FFI, although this stops shot of being inlined assembly in the sense of the C language.

    The goal for the project is to have an environment with the hardware control of assembly and the type system of Haskell. Of course, it is pretty easy to add support for other assembly constructs to Potential. The Intel reference guides provide very clear psudocode for each of the mnemonics, and typically it is pretty clear how to model an instruction’s behavior in the type system. I imagine that once the project has a more stable foundation we will see various extensions popping up as the need arises.

  5. Artyom Shalkhakov

     /  10 June, 2010

    I think that looking into TAL (typed assembly language) and DTAL (TAL enriched with a form of dependent types) would be useful as well.

  6. Kashyap

     /  12 October, 2010

    Hi,
    It’s really nice to see your initiative. I’ve been thinking in similar lines for a while now but I am yet to get my Haskell skills in place.
    I was trying to articulate this idea to barrelfish folks here – https://lists.inf.ethz.ch/pipermail/barrelfish-users/2010-February/000046.html

    I am really keen to understand more about your project and try and contribute to it.

  7. @Kashyap Thanks for your interest in Potential. The language has its own website (http://potential-lang.org) which has more information (particularly about design goals and current limitations).

    The current code that I have on github (http://github.com/intoverflow/Potential) can be thought of as a prototype for exploring the interaction between assembly and a Haskell-style type system. As mentioned in the post you read, it’s implemented as an ESDL in Haskell, which gave me an advanced type system at the cost of being unnaturally embedded in Haskell (I say “unnatural” because the Potential ESDL can’t interact with other Haskell functions at run time).

    I’m currently working on a new prototype which *isn’t* implemented embedded in Haskell. This prototype expands the language with a mixture of high- and low-level constructs: the goal is to have a high-level language which has type-safe embedded assembly.

    There isn’t much infrastructure in place right now to enable contributions, which is a shortcoming on my end. By the end of this month we will have a more coherent website inviting contributors, as well as some other tools for collaboration.

  8. Kashyap

     /  12 October, 2010

    Quick questions … Does Potential output assembly when compiled or when it is run?
    As in, I write the code in Potential (essentially Haskell) … then when I compile it, do I get assembly? or when I run it?

    Are you exploring the non-embedded route because you;ve run into a roadblock with the embedded approach?

  9. @Kashyap If you view Potential as an EDSL, then it would be right to say that it outputs assembly when it is executed. On the other hand, the Potential source contains a program (essentially a wrapper around GHC) which behaves like a compiler for Potential code; using this program, it is as though Potential compiles to assembly.

    I have encountered some unpleasant roadblocks with the embedded approach. I believe they can be overcome, but in many cases the solutions I’ve found are uncomfortable or inconvenient.

    When you’re embedded in Haskell, you’re stuck with the Haskell syntax. This is fine if your language “feels” like Haskell, but not everything fits this model. One example is the je mnemonic: remembering that Potential is based on Floyd-Hoare (FH) logic, a good question is “what’s the Floyd-Hoare type of je?” The trouble is that following the jump and not following the jump should lead to the same machine state, if je is to have a well-defined FH type. It’s easy to write down a rule that says something like “je X is a valid instruction when X :: a -> b and the code following je X is also a -> b,” but enforcing this elegantly within the confines of Haskell syntax is rather tricky.

    I want to have more progress on the new Potential compiler before making any detailed announcement about the shift away from embedding in Haskell, but ultimately it was these sorts of issues that drove me to make the move. There are other others behind the shift as well, but I’ll defer describing them until said announcement is ready.

  10. Kashyap

     /  10 November, 2010

    A follow up question – about je – would’nt a function ‘potential_if’ – that does an if-then-else – capture the je semantic?

  11. I’d say je is used also in loops.

  12. Great post! Nice!

  1. Potential publicly announced « The Potential Programming Language

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: