cabal-dev: sandboxed development builds for Haskell

Performing consistent builds is critical in software development, but the current system in GHC/Haskell of per-user and per-system GHC package databases interferes with this need for consistency. It is difficult to precisely identify the dependencies of a given project, and changes necessary to enable one project to build may render another project inoperable. If each project had a separate package database, each project could be built in a sandbox.

Galois has released cabal-dev:  a tool for managing development builds of Haskell projects within sandboxes.

Both cabal-install repositories and sandboxed ghc package databases are used to prevent interactions between disparate projects, or user package databases. cabal-dev is similar to capri, which was coincidentally developed concurrently. The two projects take slightly different approaches to sandboxing, and exhibit slightly different behaviors depending on the state of the global package database, and the versions of the tools installed.

For most packages, just use cabal-dev instead of cabal, and you will get a sandboxed build that will not install anything (even automatically installed dependencies) into the user or global ghc package databases. If your build depends on patched or unreleased libraries, you can add them to your sandboxed build environment so they can be installed by cabal-dev or cabal by running:

> cabal-dev add-source /path/to/source/code

Where /path/to/source/code is either a path to a source directory containing a .cabal file, or an sdist tarball.Cabal-dev has been in use at Galois for roughly six months now, but it should currently be treated as alpha software: we've exercised a few execution paths heavily, but it still has a number of rough edges.Cabal-dev is hosted on hackage and git-hub. A brief tutorial can be found in the README.md.

Building a business with Haskell: Case Studies: Cryptol, HaLVM and Copilot

During BelHac, the Ghent Haskell Hackathon in November, we took an afternoon session for a "Functional Programming in Industry" impromptu workshop. The following are slides I presented on Galois' experience building a business using our functional programming expertise, in particular, Haskell.

The talk describes three case studies where "functional thinking" helped shape the solution to the client's problem, whether via types, semantics, abstractions or otherwise. The examples are taken from the Cryptol, Embedded Systems and Secure Networking research programs at Galois. A PDF of the slides are also available.

Building a business with Haskell: Case Studies: Cryptol, HaLVM and Copilot

More about functional programming at Galois...

Galois releases the Haskell Lightweight Virtual Machine (HaLVM)

Galois, Inc. is pleased to announce the immediate release of the Haskell Lightweight Virtual Machine (or HaLVM), version 1.0. The HaLVM is a port of the GHC runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen’s “bare metal.” Internally, Galois has used this system in several projects with much success, and we hope y’all will have an equally great time with it.

What might you do with a HaLVM? Pretty much anything you want. :) Explore designs for operating system decomposition, examine new notions of mobile computation with the HaLVM and Xen migration, or find interesting network services and lock them inside small, cheap, single-purpose VMs.

The HaLVM is the result of many years of effort, by many people inside Galois.  Although it is not yet totally bug-free, we have decided that broad adoption wins over perfection and thus we are releasing it for general review. As such, there will be some rough edges, and we urge you to read the documentation to understand the platforms we test on.

We are releasing the HaLVM under a non-restrictive BSD3 license. You can find it here:

http://halvm.org

We welcome user feedback, feature requests, bug notices, patches, and feature additions; see the page above for guidelines on getting involved.

Finally, we’d like to give many things to the GHC and Xen communities, without which this work would not be possible.

If you have any questions or concerns, please don’t hesitate to contact the HaLVM’s maintainers at halvm-devel@community.galois.com.

Have a lovely day!

Tech Talk: Copilot: A Hard Real-Time Runtime Monitor

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:

Copilot: A Hard Real-Time Runtime Monitor (slides, video)

speaker:

Lee Pike

time:

10:30am, Tuesday, 9 November 2010

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

We address the problem of runtime monitoring for hard real-time programs---a domain in which correctness is critical yet has largely been overlooked in the runtime monitoring community. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a stream-based dataflow language that generates small constant-time and constant-space C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying real-time operating system. This talk will include fun pictures and videos.

bio:

Lee Pike has worked in Research & Development at Galois, Inc. since 2005. His primary area of research is dependable embedded systems, including both safety-critical and security-critical systems. Previously, he was a research scientist with the NASA Langley Formal Methods Group. He has a Ph.D in Computer Science from Indiana University. He has a Best Paper award from Formal Methods in Computer-Aided Design (FMCAD'2007), and service includes being on the program committees of FMCAD and Interactive Theorem Proving. His publications and other information can be found at http://www.cs.indiana.edu/~lepike.

Click to read more ...

Concurrent Orchestration in Haskell

John Launchbury presented the Orc language for concurrent scripting at the Haskell Workshop, 2010 in Baltimore.

Concurrent Orchestration in Haskell

John Launchbury

Trevor Elliott

The talk slides are available in PDF or online.

We present a concurrent scripting language embedded in Haskell, emulating the functionality of the Orc orchestration language by providing many-valued (real) non-determinism in the context of concurrent effects. We provide many examples of its use, as well as a brief description of how we use the embedded Orc DSL in practice. We describe the abstraction layers of the implementation, and use the fact that we have a layered approach to establish and demonstrate algebraic properties satisfied by the combinators.

Click to read more ...