Bluish Coder

Programming Languages, Martials Arts and Computers. The Weblog of Chris Double.


2013-08-15

Phantom Types in Rust

Update 2013-08-16, I've updated the first example based on feedback from the hacker news, /r/rust, and /r/programming threads.

I attended an overview of how the Servo browser engine, written in the Rust programming language, implements the task of laying out of elements on a web page. Patrick Walton gave the talk and highlighted some of the implementation idioms in Servo. Phantom Types are used in a number of places so I thought I'd try some phantom type examples to help learn more about Rust and Servo.

DSL type checking

Rust supports generics. A phantom type is a type parameter that isn't used in the definition of the type. Imagine a datatype that is used to represent types in a simple DSL:

enum T  { TI(int), TS(~str) }

The type T has two constructors. A TI representing an integer and a TS representing a string. In Rust the ~ prefixing str means 'owned pointer to a string allocated on the heap'.

We have two functions that operate on this type. One to add two integers and the other to concatenate two strings:

fn plus (lhs: T, rhs: T) -> T
fn concat (lhs: T, rhs: T) -> T 

Using these functions looks like:

let d1 = TI(1);
let d2 = TI(2);
let x = plus(d1, d2);
display(&x);

let d1 = TS(~"Hello, ");
let d2 = TS(~"World");
let y = concat (d1,d2);
display(&y);

Unforunately with the type definition of T it is possible to add an integer and a string:

let d1 = TI(1);
let d2 = TS(~"Hello, ");
let x = plus(d1, d2);
display(&x);

This won't be caught at compile time but, assuming the plus function aborts on incorrect types, will fail at runtime. A full example that demonstrates this available in test1.rs. Compiling with rustc test.rs and running the resulting test produces:

int: 3
str: Hello, World
task <unnamed> failed at 'error', test1.rs:12

We can detect this issue at compile time by using phantom types. This involves changing the T type to be:

enum T<A>  { TI(int), TS(~str) }

Notice that the type index A does not appear anywhere in the type definition on the right hand side. The definitions of plus and concat are changed to have a different type for the type index A:

fn plus (lhs: T<int>, rhs: T<int>) -> T<int>
fn concat (lhs: T<~str>, rhs: T<~str>) -> T<~str>

We also have to change the code that creates the TI and TS types. Code like the following will successfully typecheck:

let d1 = TI(1);
let d2 = TS(~"hello");
let x = plus(d1, d2);

This is because d1 and d2 get their types inferred as T<int> due to plus requiring two T<int> types. What's needed is to constrain the types of d1 and d2 to T<int> and T<~str> at the point of definition. This can be done with:

let d1: T<int> = TI(1);
let d2: T<~str> = TS(~"foo");
let x = plus(d1, d2);

Unfortunately this will still work:

let d1: T<int> = TI(1);
let d2: T<int> = TS(~"foo");
let x = plus(d1, d2);

A better approach is to not use the constructors for the T<A> enum and instead create our own:

fn make_int (i: int)  -> T<int>  { TI(i) }
fn make_str (s: ~str) -> T<~str> { TS(s) }

Using these to create our values will ensure that they have the type of the argument passed to the function. Passing the wrong type is now an error:

let d1 = make_int(1);
let d2 = make_str(~"foo");
let x = plus(d1, d2);

In real code it's best to ensure that the constructors for T<A> aren't public to ensure that callers from outside the module can't create them and subvert our attempts at better type checking.

This code also ensures that the result of a plus cannot be used in a concat and vice versa. The following code produces a compile error:

fn main() {
  let d1 = TI(1);
  let d2 = TI(2);
  let x = plus(d1, d2);
  display(&x);

  let d1 = TS(~"Hello, ");
  let d2 = TS(~"World");
  let y = concat (d1,d2);
  display(&y);

  // Compile error here
  let z = concat(x, y);
  display(&z);
}

The full example is in test2.rs and compiling it results in:

test2.rs:45:17: 45:18 error: mismatched types:
  expected `T<~str>` but found `T<int>` (expected ~str but found int)
test2.rs:45   let z = concat(x, y);
                         ^

Commenting out the offending code allows the program to compile and run without errors. There is no runtime overhead or additional code generated when using phantom types. The types are erased at compile time and the resulting program is as if they hadn't been used at all - except that you know the code won't have the runtime failure as it passed type checking.

Safer strings

Another use of phantom types is for providing a taint to string types so they can't be used in an unsafe manner. An example of this is generating HTML template pages as the response to an HTTP request. The page is generated by concatenating various strings together. A string that comes from user input must be properly escaped before it is allowed to be embedded in an HTML page.

In this example we have a type representing an HTML fragment used to compose an HTML page to be generated:

enum Fragment { Str(~str) }

It only has one constructor, Str, which holds the unique string containing the page data. A render_page function displays a complete page:

fn get_str(s: Fragment) -> ~str {
  match s {
    Str(s) => { s }
  }
}

fn render_page(s: Fragment) {
  println(get_str(s));
}

Functions exist to generate the head and body of the page with the latter including some form of data obtained elsewhere. Perhaps user input or the output of some other process:

fn get_head() -> Fragment {
  Str(~"<head></head>")
}  

fn get_body(s: Fragment) -> Fragment {
  Str("<body>" + get_str(s) + "</body>")
}

Data from untrusted sources needs to be 'blessed'. This should perform any escaping necessary to make the data safe to embed in the web page. The following is a main program that generates and displays the page:

fn main() {
  let user_input = get_user_input(~"<script>alert('oops')</script>");
  let page = generate_page(get_head(),
                           get_body(user_input));
  render_page(page);
}

This compiles and runs. The full example for trying it out is in test3.rs. The output is:

<html><head></head><body><script>alert('oops')</script></body></html>  

Unfortunately we forgot to call bless and the user input was added unescaped. Ideally this should be a compile time error. If we add a phantom type to the Fragment class we can differentiate between safe and unsafe strings with no runtime overhead:

struct Safe;
struct Unsafe;

enum Fragment<T> { Str(~str) }

All the generation functions now require safe fragments:

fn generate_page(head: Fragment<Safe>, body: Fragment<Safe>) -> Fragment<Safe>
fn get_head() -> Fragment<Safe>
fn get_body(s: Fragment<Safe>) -> Fragment<Safe>
fn render_page(s: Fragment<Safe>)
fn bless(s: Fragment<Unsafe>) -> Fragment<Safe>

The exception is the function that obtains untrusted data. It returns an unsafe fragment:

fn get_user_input(s: ~str) -> Fragment<Unsafe>

Now the code that forgets to call bless (in test4.rs) results in a compile error:

test4.rs:41:36: 41:46 error: mismatched types: expected `Fragment<Safe>`
   but found `Fragment<Unsafe>` (expected struct Safe but found struct Unsafe)
test4.rs:41                            get_body(user_input));
                                            ^~~~~~~~~~

This approach can be used to help wherever untrusted data shouldn't be mixed with trusted data. Constructing SQL queries and generating URL's are other examples.

Servo

One of the uses of phantom types in Servo is in the Node type:

// A phantom type representing the script task's view of this node. Script is able to mutate
/// nodes but may not access layout data.
pub struct ScriptView;

/// A phantom type representing the layout task's view of the node. Layout is not allowed to mutate
/// nodes but may access layout data.
pub struct LayoutView;

/// An HTML node.
///
/// `View` describes extra data associated with this node that this task has access to. For
/// the script task, this is the unit type `()`. For the layout task, this is
/// `layout::aux::LayoutData`.
pub struct Node<View> {
  ...
}

A node has fields that should only be accessed or mutated on certain tasks. The script task can mutate nodes but cannot access data related to layout. The layout task is not allowed to mutate the node but can access the layout data. The prevents data races amongst the fields in the node.

The is implemented using phantom types. The node type is indexed over a View which can be ScriptView or LayoutView. There are methods implemented for Node<ScriptView> which makes them only accessible to the script task:

impl Node<ScriptView> {
  pub fn ....
}

An example of where the layout task gets the LayoutView version of a node is in handle_reflow. This takes a Reflow structure:

pub struct Reflow {
    /// The document node.
    document_root: AbstractNode<ScriptView>,
    /// The style changes that need to be done.
    damage: DocumentDamage,
    /// The goal of reflow: either to render to the screen or to flush layout info for script.
    goal: ReflowGoal,
    /// The URL of the page.
    url: Url,
    /// The channel through which messages can be sent back to the script task.
    script_chan: ScriptChan,
    /// The current window size.
    window_size: Size2D<uint>,
    /// The channel that we send a notification to.
    script_join_chan: Chan<()>,
}

Note the document_root is an AbstractNode<ScriptView>. Inside the handle_reflow function in the layout task it does:

/// The high-level routine that performs layout tasks.
fn handle_reflow(&mut self, data: &Reflow) {
    // FIXME: Isolate this transmutation into a "bridge" module.
    let node: &AbstractNode<LayoutView> = unsafe {
        transmute(&data.document_root)
    };
    ...
}

The function transmute is a cast. In this case it is converting the AbstractNode<ScriptView> to an AbstractNode<LayoutView>. The rest of the reflow deals with this so it can be proven to not access the script portions of the node and therefore should not have data races in those parts.

Node simplified

I've attempted to do a simplified example in Rust to test this type of phantom type usage. In layout.rs I have a basic Node class that is indexed over the views:

pub struct ScriptView;
pub struct LayoutView;

pub struct LayoutData {
  field3: ~str,
}

impl LayoutData {
  pub fn new() -> LayoutData {
    LayoutData { field3: ~"layoutdata" }
  }
}

pub struct Node<View> {
  field1: ~str,
  field2: ~str,

  priv layout_data: Option<@mut LayoutData>
}

Note that layout_data is private. A method implemented on Node<LayoutView> provides public access to it:

impl Node<LayoutView> {
  pub fn layout_data(&self) -> Option<@mut LayoutData> {
    self.layout_data
  }
}

Only the layout task has the LayoutView of Node so only it can get access to the layout_data method. A LayoutView is obtained by casting (using transmute):

impl<View> Node<View> {
  pub fn change_view<View>(&self) -> &Node<View> {
    unsafe {
      transmute(self)
    }
  } 
}

The file main.rc contains the main function that tests these layout types and functions:

mod layout;

pub fn main() {
  use layout::*;

  let a = ~Node::new();
  std::io::println (a.field1);
  std::io::println (a.field2);
  let b: &Node<LayoutView> = a.change_view();
  match (b.layout_data()) {
    None => { std::io::println("no layout data"); }
    Some (data) => { std::io::println(data.field3); }
  }
}

This shows accessing the fields from the ScriptView view of the Node then switching to the LayoutView to get access to the layout_data. Trying to modify the non-layout fields with the LayoutView should fail. Build the example with rustc main.rc and make sure main.rc and layout.rs are in the current directory.

The Servo code is quite a bit more complex than this but hopefully it helps with understanding the idiom of phantom type usage in nodes. If I've made any mistakes in my understanding of how things work, please let me know!

Resources

Some resources I used in writing this post:

Tags: mozilla  rust 

2013-08-08

Linking and calling Rust functions from C

At a recent functional programming meetup I was discussing with a colleague about how nice it would be to be able to use Rust in Gecko. This made me curious if it was possible to implement libraries in Rust and call them from C. After the meeting I asked in #rust and got pointed to some projects that showed the way.

This lead me to trying to come up with as simple example as possible of compiling a Rust file into an object file, linking it to a C program and running it without the Rust runtime. The code is in my rust-from-c-example github repository. It can be cloned and built with:

$ git clone http://github.com/doublec/rust-from-c-example
$ cd rust-from-c-example
$ make
$ ./test

To avoid issues with integrating with the Rust runtime I've opted to not use it. This means no threads and limits the standard library usage. This example is very simple, only demonstrating adding two numbers. Extending from this will be an interesting exercise to see how much Rust can be used.

The Rust code is:

#[crate_type = "lib"];
#[no_std];
#[allow(ctypes)];

#[no_mangle]
pub extern fn add(lhs: uint, rhs: uint) -> uint {
  lhs + rhs
}

The first three lines ensure that the file is compiled as a library, does not use the standard library and can use C types. The no_mangle declaration stops the Rust default of mangling function names to include their module and version information. This means that add in Rust is exported as add for C programs. The extern makes the function available from C and defaults to cdecl calling format.

To generate a .o file that can be linked into a C program:

$ rustc -c mylib.rs

The C program creates an extern declaration for add and calls it:

#include <stdio.h>

extern unsigned int add(unsigned int lhs, unsigned int rhs);

int main() {
  printf("add(40,2) = %u\n", add(40,2));
  return 0;
}

Unfortunately we can't just compile and link with the mylib.o file. This results in a linker error:

mylib.o: In function `add':
mylib.rc:(.text+0x4f): undefined reference to `upcall_call_shim_on_rust_stack'
collect2: error: ld returned 1 exit status

Some searching pointed me to armboot which had a stub implementation for this in zero.c. Compiling and linking to that worked successfully. A cut down variant of zero.c is included in the project.

There's a bunch of limitations with this approach. We're basically using Rust as a higher level C. This post on embedding Rust in Ruby details some of the limitations:

When calling Rust code you will not be executing in a Rust task and will not have access to any runtime services that require task-local resources. Currently this means you can't use the local heap, nor can you spawn or communicate with tasks, nor call fail!() to unwind the stack. I/O doesn't work because core::io (unfortunately, and incorrectly) uses @-boxes. Even logging does not work. Calling any code that tries to access the task context will cause the process to abort. Because code is not executing in a task, it does not grow the stack, and instead runs on whatever stack the foreign caller was executing on. Recurse too deep and you will scribble on random memory.

Hopefully some of these limitations will go away or 'zero runtime' libraries will appear to make this sort of usage easier. Some resources that helped putting this together were:

Tags: mozilla  rust 

2013-07-01

Constructing Proofs with dataprop in ATS

My last post that covered using proofs in ATS implemented a stack. In this post I step back a bit and go through some smaller examples using dataprop with proofs using prfun. The examples I work through here are based on the Propositions and Evidence section of Software Foundations. That book covers the Coq Proof Assistant and I've been working through some of the exercises in ATS.

The Propositions and Evidence chapter starts off with introducing a property of natural numbers. Numbers with this property are considered 'beautiful'. A natural number is 'beautiful' if it is 0, 3, 5 or the sum of two beautiful numbers. This is defined in four rules:

  • Rule b_0: The number 0 is beautiful.
  • Rule b_3: The number 3 is beautiful.
  • Rule b_5: The number 5 is beautiful.
  • Rule b_sum: If n and m are beautiful, then so is their sum.

This can be expressed in ATS using dataprop:

dataprop BEAUTIFUL (n:int) =
| B_0 (0)
| B_3 (3)
| B_5 (5)
| {m,n:nat} B_SUM (n+m) of (BEAUTIFUL m, BEAUTIFUL n)

A dataprop is similar to a datatype but exists for the proof system. Like other proof elements (prfun, etc) they are erased at compile time and have no runtime overhead. A dataprop is used to encode a relation or proposition. The BEAUTIFUL dataprop uses dependent types - it has a natural number, n, as a type index, making BEAUTIFUL a property of numbers. Each line implements the rules outlined earlier.

In the B_SUM line the section in curly brackets, {m,n:nat}, declares two universal variables. This line should be read as "For all m and and n, which are natural numbers that are beautiful, the sum of those numbers are also beautiful".

Now that we have the proposition we can start assembling proofs. The first proof we look at is proving the second rule - that the number 3 is beautiful. We need to implement this proof function:

prfun three_is_beautiful ():<> BEAUTIFUL 3

A proof function, introduced with prfun or prfn is used to implement proofs that are checked by ATS to ensure programs are correct. prfn is used for non-recursive functions whereas prfun can be recursive. If it is recursive it must be able to prove it can terminate. How this is done will be explained later. This function returns an instance of BEAUTIFUL 3. The :<> section of the definition means that this function is a pure function. It can perform no side effects. All proof functions must be pure and terminating.

The implementation for this proof is simple:

prfn three_is_beautiful ():<> BEAUTIFUL 3 = B_3

The body just returns the B_3 rule. Typechecking this succeeds:

$ atscc -tc proof.dats
The file [proof.dats] is successfully typechecked!

It is possible to declare proof functions but not implement them. This is a way of saying to the compiler that "the proof is self evident". It can be used in cases where proofs are time consuming to implement but nevertheless obvious. In this case, three_is_beautiful is obvious from the rules so we could just declare it without an implementation:

praxi three_is_beautiful ():<> BEAUTIFUL 3

Note here I use praxi instead of prfun. The former is often used for fundamental axioms that don't need to be proved. They are not expected to be implemented. Although the ATS compiler doesn't currently warn if a prfun is unimplemented it may do in the future so it's good practice to use praxi for proofs that aren't intended to be implemented.

The next step up would be to prove some aspect using B_SUM. Let's prove that eight is a beautiful number:

prfn eight_is_beautiful ():<> BEAUTIFUL 8 = B_SUM (B_3, B_5)

The implementation for this constructs a B_SUM of two other BEAUTIFUL rules, B_3 and B_5. Typechecking this confirms that this is enough to prove the rule.

Proof functions can be used to prove (or disprove) claims. For example, someone claims that adding three to any beautiful number will produce a beautiful number. Expressed as a proof function:

prfn b_plus3 {n:nat} (b: BEAUTIFUL n):<> BEAUTIFUL (3+n)

The implementation is trivial and successful typechecking by the ATS compiler proves that any beautiful number, with three added, does indeed produce a new beautiful number:

prfn b_plus3 {n:nat} (b: BEAUTIFUL n):<> BEAUTIFUL (3+n) =
  B_SUM (B_3, b)

Another claim to prove is that any beautiful number multiplied by two produces a beautiful number. The claim, implemented as a proof is:

prfn b_times2 {n:nat} (b: BEAUTIFUL n):<> BEAUTIFUL (2*n) =
  B_SUM (b, b)

A more complicated proof is that any beautiful number multiplied by any natural number is a beautiful number:

prfun b_timesm {m,n:nat} .<m>. (b: BEAUTIFUL n):<>
       [p:nat] (MUL (m,n,p), BEAUTIFUL p) =

This is the first proof function we've looked at that needs recursion. Recursive proof functions must show they can terminate. This is done by adding a termination clause (the bit between .< and >.). The termination clause must contain a static type variable that is used in each recursive call and can be proven to decrement on each call. In this case it is m.

The return result of this proof function includes an existential variable, p and returns a tuple of a MUL proof object and the beautiful number. MUL is part of the ATS prelude. It encodes the relation that for any numbers m and n the number p is m*n. The p here is also included as the type index of the beautiful number returned. The proof then reads as "For all m which are natural numbers, and for all n which are beautiful numbers, there exists a beautiful number p that is m*n".

The implementation of this proof looks like:

sif m == 0 then
  (MULbas, B_0)
else let
  prval (pf, b') = b_timesm {m-1,n} (b)
in
  (MULind pf, B_SUM(b, b'))
end

The first thing you may note is we use sif instead of if. The former is for the static type system which is what the variables m and n belong to. In the case of 0 (multiplying a beautiful number by zero) we return the B_0 rule and the base case for the MUL prop.

In the case of non-zero multiplication we recursively call b_timesm, reducing m on each call. As m and n are universal variables in the static type system they are passed using the {...} syntax. The result of this is summed. We are implementing multiplication via recursive addition basically. More on the use of MUL can be read in the encoding relations as dataprops section of the ATS documentation.

Once we've proven what we want to prove with regards to beautiful numbers, how are they used in actual programs? Imagine a program that needs to add beautiful numbers and display the result. Without any checking it could look like:

fun add_beautiful (n1: int, n2: int): int =
  n1 + n2

fun do_beautiful () = let
  val n1 = 3
  val n2 = 8
  val n3 = add_beautiful (n1, n2)
in
  printf("%d\n", @(n3))
end

This relies on inspection to ensure that numbers are in fact beautiful numbers. Or it could use runtime asserts to that effect. The same program using the proofs we've defined would be:

fun add_beautiful {n1,n2:nat}
         (pf1: BEAUTIFUL n1, pf2: BEAUTIFUL n2
          | n1: int, n2: int): [n3:nat] (BEAUTIFUL n3 | int) =
  (B_SUM (pf1,pf2) | n1 + n2)

fun do_beautiful () = let
  prval pf1 = three_is_beautiful ()
  prval pf2 = eight_is_beautiful ()
  val n1 = 3
  val n2 = 8
  val (pf3 | n3) = add_beautiful (pf1, pf2 | n1, n2)
in
  printf("%d\n", @(n3))
end

This program will not compile if non-beautiful numbers are passed to add_beautiful. We've constructed proofs that the two numbers we are using are beautiful and pass those proofs to the add_beautiful function. It returns the sum of the two numbers and a proof that the resulting number is also a beautiful number.

An exercise for the reader might be to implement an 'assert_beautiful' function that checks if a given integer is a beautiful number using proofs to verify the implementation is correct. The function to implement would allow:

extern fun assert_beautiful (n: int): [n:nat] (BEAUTIFUL n | int n)

fun do_beautiful2 (a:int, b:int): void = let
  val (pf1 | n1) = assert_beautiful (a)
  val (pf2 | n2) = assert_beautiful (b)
  val (pf3 | n3) = add_beautiful (pf1, pf2 | n1, n2)
in
  printf("%d\n", @(n3))
end

As noted in Software Foundations, besides constructing evidence that numbers are beautiful, we can also reason about them using the proof system. The only way to build evidence that numbers are beautiful are via the constructors in the dataprop. In the following example we create a new property of numbers, gorgeous numbers, and prove some relationships with beautiful numbers.

dataprop GORGEOUS (n:int) =
| G_0 (0)
| {n:nat} G_plus3 (3+n) of GORGEOUS (n)
| {n:nat} G_plus5 (5+n) of GORGEOUS (n)

I'll leave as a reader exercise to write some proofs about gorgeous numbers in a similar way we did with beautiful numbers. Try proving that the sum of two gorgeous numbers results in a gorgeous number.

One proof I'll demonstrate here is proving that all gorgeous numbers are also beautiful numbers. Looking at the definition gives an intuitive idea that this is the case. A proof function to prove it looks like:

prfun gorgeous__beautiful {n:nat} (g: GORGEOUS n): BEAUTIFUL n

The implementation uses case+ to dispatch on the possible constructors of GORGEOUS and produce BEAUTIFUL equivalents:

prfun gorgeous__beautiful {n:nat} .<n>. (g: GORGEOUS n): BEAUTIFUL n = 
  case+ g of 
  | G_0 () => B_0
  | G_plus3 g => B_SUM (B_3, gorgeous__beautiful (g))
  | G_plus5 g => B_SUM (B_5, gorgeous__beautiful (g))

This will fail to type check if gorgeous numbers are not also beautiful numbers. It does pass typechecking so we know that this is the case.

Tags: ats 

2013-06-11

Editing remote files with Acme in Inferno OS

Inferno OS ships with a version of the acme text editor. I've tried to use acme on and off for a bit and it never stuck. I've always been a vim and emacs user. Recently I watched a video by Russ Cox called A Tour of Acme that motivated me to try it again.

The video is short and covers a lot of what makes Acme interesting. Most of it is related to the extensibility of the editor via shell commands dealing with piped input and output alongside the power of sam editing commands.

Some useful acme papers and tutorials are:

For a recent task I had restored a backup of my Creatures Developer Resource website, recovering from a hard drive failure. I wanted to remove the Google ad code from each page of the website.

To do this from within Inferno and using Acme I first ensured I had the styx service running on the remote web server and had the host file system bound so remote users could connect to it:

; bind '#U*' /mnt/host
; svc/styx

On my client Inferno machine I mounted this remote directory and ran acme to edit the files on it.

% mount tcp!example.com!styx /n/host
% acme

The acme editor starts and from here I can edit files on the remote server by accessing /n/host/mnt/host. The first step was to load all HTML files in the webserver directory into acme. This was done by executing the following command in an acme window that had its location set to /n/host/mnt/host/var/www/example.com (using mouse button 2 to execute):

Edit B <du -an|grep 'html?$'

From the Sam Reference it can be seen that B is used to load files into the editor. In this case I load the output of the command du -an|grep 'html?$'. The command du -an provides a recursive list of all files in the current directory and subdirectories and the grep limits it to those ending in htm or html. Once executed acme has loaded all the files we're interested in from the remote server.

The Google Ad snippet to be removed looks like:

<!-- Gooogle -->
...
<!-- Gooogle -->

The following sam command will find this snippet and delete it:

,x<!-- Gooogle -->(.|\n)*<!-- Gooogle -->/ d

The , means the starting range is the entire file. The x command executes another comand for each part of the range that matches the regular expression - in this case the entire Google Ad snippet. The command to execute for each match is d which is to delete the region. To have acme run this on all open HTML files I used:

Edit X/html?$/ ,x<!-- Gooogle -->(.|\n)*<!-- Gooogle -->/ d

The X command iterates over all open windows with the name matching the regular expression and runs the following command, which I described above. This results in all the ad snippets from being removed from all the HTML files. To save them back to disk:

Edit X/html?$/ w

And to close the acme windows:

Edit X/html?$/ D

The task is done, closing acme and unmounting the remote file system:

% unmount /n/host

This task was pretty simple and could be done with a number of existing Unix tools but I wanted to give Acme a try with a real world task. It worked well editing remote files, and iterating towards the correct sam commands to use was easy by interactively testing on single files and using the p command to print ranges instead of deleting. Make sure authentication is set up before sharing remote files though!

Tags: inferno  acme 

2013-06-05

Remote Shells with Inferno OS

Inferno OS provides a mechanism to connect to remote computers and execute commands similar to the way SSH works on Unix systems. The command to do this is cpu. This can be used to execute commands, start a remote shell, and share GUI applications.

To use cpu you'll need to set up authentication and encryption. This provides the mechanism to authentiate to the remote machine and encrypt the session data.

The rstyx command needs to be run on the remote host to start the services that cpu uses to connect:

; ndb/cs
; ndb/dns
; svc/rstyx

The ndb commands shown there start the services to use the network and DNS. Usually this is started beforehand but I list them for completeness.

With rstyx running and authentication configured the client can connect to the remote machine using cpu:

% cpu example.com
; ...now on server...

This creates a session that is encrypted during authentication but then unencrypted. To use an encrypted session the -C flag is required:

% cpu -C rc4_256 example.com
; ls
; ...server directory listing...

cpu takes an optional argument, that defaults to the shell, to execute:

% cpu -C rc4_256 example.com ls
; ...server directory listing...
%

The namespaces available to the cpu command are mapped to the directory /n/client/ in a cpu session. This means the remote shell or command can use resources on the client. For example a phone running Inferno can cpu to a remote host and that remote host can make calls, send messages, etc using the phones resources. By controlling what namespaces exist before cpu is called the client can restrict what resources are available in the remote session.

Another example of resource sharing is to run GUI programs on the server but have the display appear on the client, similar to how X11 forwarding operates. Doing this requires having the wm window mananger on the client export its interface to a namespace (it's one of the few applications that doesn't do this by default on Inferno) and then in the cpu session bind that to a location that GUI programs can see. On the client the export would look like:

; mount {wmexport} /mnt/wm
; cpu -C rc4_256 example.com
; wmimport -w /n/client/mnt/wm acme &

This runs the editor acme on the server but the display is shown on the client. The -w flag passed to wmimport gives the path to an exported directory provided by wmexport. In this case we use the directory exported on the client which cpu has exposed under /n/client/mnt/wm.

Any graphical program can be run this way including GUI shells, games, etc. Unfortunately, like X11 forwarding, it's fairly slow over low bandwidth connections. For local connections it's quite usable however. This could be a useful way to share a phone application on a desktop or a desktop application on a phone when it's connected to the same network.

A combination of resources on the remote server and the client can be used to work around the low bandwidth issue. The acme editor exposes directories and files to control the editor. By running acme on the client, cpu-ing to the remote server so it can see these directories, the programs on the remote end can send data to the client acme window. An example follows:

; acme
; ...create a terminal in acme by 2nd-button clicking `win`...
; ...in the acme terminal window...
; cpu -C rc4_256 cd.pn

Now the remote session running inside acme will expose the needed interfaces to control the client acme program via /n/client/mnt/acme:

; echo Hello >/n/client/mnt/acme/new/body

This command, executed on the server in the remote session, creates a new window in the client acme program with the text "Hello".

Tags: inferno 


This site is accessable over tor as hidden service 6vp5u25g4izec5c37wv52skvecikld6kysvsivnl6sdg6q7wy25lixad.onion, or Freenet using key:
USK@1ORdIvjL2H1bZblJcP8hu2LjjKtVB-rVzp8mLty~5N4,8hL85otZBbq0geDsSKkBK4sKESL2SrNVecFZz9NxGVQ,AQACAAE/bluishcoder/-61/


Tags

Archives
Links