Skip to content

Commit

Permalink
Merge branch 'main' of https://github.com/PrincetonUniversity/lucid i…
Browse files Browse the repository at this point in the history
…nto main
  • Loading branch information
jsonch committed Jul 26, 2024
2 parents b02977c + 9aeff3a commit 7213297
Show file tree
Hide file tree
Showing 8 changed files with 124 additions and 143 deletions.
9 changes: 5 additions & 4 deletions tutorials/interp/01monitor/makefile
Original file line number Diff line number Diff line change
Expand Up @@ -18,20 +18,21 @@ endif

.PHONY: interp interp_local build_p4 clean dptc force current_makefile

# run the lucid interpreter on SRC, using the dockerized lucid.sh script.
interp:
@$(LUCID_SH) interp $(SRC)

# run the lucid interpreter on SRC, using the local build
# of the lucid interpreter (which is named dpt)
interp_local:
interp:
@if [ "$(DPT)" = "-" ]; then \
echo "local dpt not found. falling back to docker"; \
$(LUCID_SH) interp $(SRC); \
else \
$(DPT) $(SRC); \
fi

# run the lucid interpreter on SRC, using the dockerized lucid.sh script.
interp_docker:
@$(LUCID_SH) interp $(SRC)

# everything below is related to compiling
# lucid to P4-tofino. Ignore if you are only
# using the interpeter.
Expand Down
10 changes: 3 additions & 7 deletions tutorials/interp/01monitor/readme.md
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ The most important part of an interpreter specification file is the list of inpu

#### Usage

Finally, to run the program, make sure that you have docker and the lucid-docker image installed, then run `make interp`.
Finally, run the program with `make interp`. Or, if you're using docker, `make interp_docker`

**Expected output**

Expand Down Expand Up @@ -106,14 +106,10 @@ Switch 0 : {

**reading the intepreter output**

The first few lines from `make interp` are output from the lucid.sh script, where it is generating the docker command to run. e.g., up to:
``
running command: docker run --rm -it --mount type=bind,source=/Users/jsonch/Desktop/gits/lucid/tutorials/interp/01monitor/monitor.dpt,target=/app/inputs/monitor.dpt --mount type=bind,source=/Users/jsonch/Desktop/gits/lucid/tutorials/interp/01monitor/monitor.json,target=/app/inputs/monitor.json jsonch/lucid:lucid /bin/sh -c "./dpt /app/inputs/monitor.dpt --spec /app/inputs/monitor.json"
``

Next, the lines prefixed with `dpt:` are messages from the lucid compiler frontend as it type checks and transforms the program into a simpler form that the interpreter can run. If your program has an error, typically the interpreter will print an error message and halt at some point in between these messages.
The lines prefixed with `dpt:` are messages from the lucid compiler frontend as it type checks and transforms the program into a simpler form that the interpreter can run. If your program has an error, typically the interpreter will print an error message and halt at some point in between these messages.

Finally, after the `dpt: Simulating...` line, we see the output of the lucid simulator. The simulator's output has two components:

1. a trace summarizing the events that were handled at each switch in the simulation, interleaved with any "printf" statements that executed in the program. In this example, the trace is:
```
t=0: Handling packet event eth_ip(11,22,2048,1,2,128) at switch 0, port 0
Expand Down
54 changes: 29 additions & 25 deletions tutorials/interp/02filter/filter.dpt
Original file line number Diff line number Diff line change
Expand Up @@ -23,30 +23,32 @@ event report(int src, int dst, int<16> len) {skip;}
/********** Tables *********/
// When you call a table, it will
// execute a pre-installed action.
// Action constructors are used to
// build those actions.
action_constr mk_result(bool b) = {
return action bool acn () {
return b;
};
};

// Tables have types. A table's type
// specifies the size of its keys,
// the types of the arguments to actions
// and the type of the action's return value.
table_type filter_table_t = {
key_type: (int, int)
arg_type: ()
ret_type: bool
// Actions have two sets of parameters.
// The first set of parameters are bound
// when the action is installed into the table;
// the second set of parameters is bound
// when the action is called by Table.lookup.
action bool mk_result(bool b)() {
return b;
}

global filter_table_t filter_table =
table_create<filter_table_t>(
(mk_result),
1024,
mk_result(false)
);

type key_t = {
int s;
int d;
}

/*
Table.t's type args (inside the << >>):
1. key type
2. action install-time argument type
3. action run-time argument type
4. action return type

Table.create(num_entries, possible_actions (list), default_action, default_action_installtime_arg);
*/
global Table.t<<key_t, bool, (), bool>> filter_table = Table.create(1024, [mk_result], mk_result, false);



/********** Filtering functions *********/
Expand Down Expand Up @@ -74,10 +76,12 @@ fun bool filter_with_match(ip_t ip) {


fun bool filter_with_table(ip_t ip) {
bool r = table_match(
/* Table.lookup(table, key, action_runtime_arg); */
bool r = Table.lookup(
filter_table,
(ip#src, ip#dst),
());
{s=ip#src; d=ip#dst},
() // () just means there is no runtime argument
);
return r;
}

Expand Down
9 changes: 5 additions & 4 deletions tutorials/interp/02filter/makefile
Original file line number Diff line number Diff line change
Expand Up @@ -18,20 +18,21 @@ endif

.PHONY: interp interp_local build_p4 clean dptc force current_makefile

# run the lucid interpreter on SRC, using the dockerized lucid.sh script.
interp:
@$(LUCID_SH) interp $(SRC)

# run the lucid interpreter on SRC, using the local build
# of the lucid interpreter (which is named dpt)
interp_local:
interp:
@if [ "$(DPT)" = "-" ]; then \
echo "local dpt not found. falling back to docker"; \
$(LUCID_SH) interp $(SRC); \
else \
$(DPT) $(SRC); \
fi

# run the lucid interpreter on SRC, using the dockerized lucid.sh script.
interp_docker:
@$(LUCID_SH) interp $(SRC)

# everything below is related to compiling
# lucid to P4-tofino. Ignore if you are only
# using the interpeter.
Expand Down
103 changes: 42 additions & 61 deletions tutorials/interp/02filter/readme.md
Original file line number Diff line number Diff line change
Expand Up @@ -113,47 +113,61 @@ Match tables are powerful, but a little more complicated than match statements.
**declaring and using tables**
`filter.dpt`, has a table named `filter_match`. To create the filter table, we call the `table_create` constructor. It takes three arguments: a list of _action constructors_, functions that can be used to produce actions for the table to call; a size (the number of cases it holds), and a default action to execute. It creates the table named "filter_table". The `global` annotation on `filter_table` means that the variable is accessible from any handler and its contents persist across events.
`filter.dpt`, has a table named `filter_match`. To create the filter table, we call the `Table.create` constructor, which produces a value of type `Table.t`.
```c
// create the filter_table
global filter_table_t filter_table =
table_create<filter_table_t>(
(mk_result), // result is an action generator that can be called to produce new actions for rules in this table. Tables can have multiple action generators.
1024, // the maximum number of rules in the table.
mk_result(false) // the default action of this table is to call the action generated by result(false)
);
global Table.t<<key_t, bool, (), bool>> filter_table = Table.create(1024, [mk_result], mk_result, false);
```
The arguments to `Table.create` are:

Next, take a look at the action constructor, `mk_result`, that `filter_table` uses:
1. number of entries (`1024`)
2. the actions that the table may use (`[mk_result]`)
3. the default action (`mk_result`)
4. an install-time argument for the default action (`false`)

```c
action_constr mk_result(bool b) = {
return action bool acn () {
return b;
};
};
```
A table's type is parametric. The parameters define the shape of the key and the action functions that the table may use. There are 4 parameter to `Table.t`:

`mk_result` takes a boolean argument `b` and uses it to construct an action named `acn` that takes no arguments and always returns `b`. The important thing to keep in mind here is that `b` gets set to a value when an action is _installed_.
1. the type of the key
2. the type of the table's actions install-time argument
3. the type of the table's actions run-time argument
4. the return type of the table's actions

To use the filter table, we call Lucid's builtin `table_match` function, which takes three arguments: the name of the table to apply, a key to match against the rules of the table, and a list of arguments to pass to whatever action the table ends up calling. `table_match` will find the first rule that matches the key, call its action, and return whatever the action returned.

Next, take a look at the action, `mk_result`, that `filter_table` uses:

```c
// use the filter_table
fun bool filter_with_table(ip_t ip) {
bool r = // return value from the matching rule
table_match(
filter_table, // the table, which holds rules and actions
(ip#src, ip#dst), // the key to match with the table
() // arguments to the table's actions
);
return r;
action bool mk_result(bool b)() {
return b;
}
```
When we call table_match on `filter_table`, the last argument is an empty list -- this is because for all the actions in `filter_table` (just `result` here), the second set of arguments is empty.
Actions take two arguments. The first set of arguments (`(bool b)` in `mk_result`) are arguments bound when a rule with that action is _installed_ into a table.
The second set of arguments (`()` for `mk_result`, which just means "no argument") are arguments bound when the action is _called_ at runtime.
So an action has both _install time_ and _run time_ arguments.
Use the filter table with `Table.match`:
```
bool r = Table.lookup(
filter_table,
{s=ip#src; d=ip#dst},
()
);
```
The first argument is the name of the table, the second argument is the key, and the third argument is the runtime argument to pass to the action.
Table.lookup's semantics are basically:
```
def table_lookup(tbl, key, arg):
# invoke first matching rule
for entry in tbl.entries:
if(equal_keys(key, entry.key)):
return entry.action(entry.install_arg, arg)
# if nothing matched, call default action
return tbl.default(tbl.default_install_arg, arg)
```
**installing table rules**
Expand All @@ -174,36 +188,3 @@ Again, the main point of tables versus match statements is that the rules in a t
This command says, "Run Table.install to add a rule to `filter_table`. The rule matches on the key `[1, 2]` and when it matches it calls the action generated by `result(true)`".
It is roughly equivalent to having a case in a match statement
`1, 2 -> {return (mk_result(true))();}`

**table types**

A final detail about tables. Looking at the declaration of `filter_table` closely, you will notice that the filter table has its own type, `filter_table_t`:

```c
global filter_table_t filter_table = ...;
```

`filter_table_t` is defined as:

```c
table_type filter_table_t = {
key_type: (int, int)
arg_type: ()
ret_type: bool
}
```

You can think of a "table type" like `filter_table_t` as a schema that defines the columns of a table: the type of each field in the table's key; the types of the parameters of all of the table's actions; and the type of the return values from all of the table's actions.

Lucid makes us specify table types for two reasons. First, because we need to know all of these details about the table at compile time so that we can allocate enough memory for it (in data plane hardware, there is no dynamic memory allocation!). Second, table types let lucid ensure that a program always uses tables in safe and well-defined ways.

Specifically, when you call `table_match` on something of type `filter_table_t`, lucid will check that:

1. the key argument of the `table_match` call is a tuple of two integer expressions

2. the "action argument" argument of the `table_match` call is an empty tuple, because of `arg_type: ()`;

3. the return value of `table_match` will always be a bool, because of `ret_type : bool`.



29 changes: 8 additions & 21 deletions tutorials/interp/03counter/counter.dpt
Original file line number Diff line number Diff line change
Expand Up @@ -21,32 +21,19 @@ event get_report(int src, int dst); // get_report is sent by the monitoring serv
event report(int src, int dst, int<32> count) {skip;} // report is sent back to the monitoring server.

/**** Indexing table -- map a flow to an integer index ****/
action_constr mk_flow_idx(int idx) = {
return action int flow_idx () {
return idx;
};
};


table_type indexing_table_t = {
key_type: (int, int)
arg_type: ()
ret_type: int
action int mk_flow_idx(int idx)() {
return idx;
}

global indexing_table_t idx_tbl =
table_create<indexing_table_t>(
(mk_flow_idx),
1024,
mk_flow_idx(0)
);
type key_t = {
int s;
int d;
}

global Table.t<<key_t, int, (), int>> idx_tbl = Table.create(1024, [mk_flow_idx], mk_flow_idx, 0);

fun int get_idx_exact(int src, int dst) {
return table_match(
idx_tbl,
(src, dst),
());
return Table.lookup(idx_tbl, {s=src; d=dst}, ());
}

/**** the flow counter array ****/
Expand Down
9 changes: 5 additions & 4 deletions tutorials/interp/03counter/makefile
Original file line number Diff line number Diff line change
Expand Up @@ -18,20 +18,21 @@ endif

.PHONY: interp interp_local build_p4 clean dptc force current_makefile

# run the lucid interpreter on SRC, using the dockerized lucid.sh script.
interp:
@$(LUCID_SH) interp $(SRC)

# run the lucid interpreter on SRC, using the local build
# of the lucid interpreter (which is named dpt)
interp_local:
interp:
@if [ "$(DPT)" = "-" ]; then \
echo "local dpt not found. falling back to docker"; \
$(LUCID_SH) interp $(SRC); \
else \
$(DPT) $(SRC); \
fi

# run the lucid interpreter on SRC, using the dockerized lucid.sh script.
interp_docker:
@$(LUCID_SH) interp $(SRC)

# everything below is related to compiling
# lucid to P4-tofino. Ignore if you are only
# using the interpeter.
Expand Down
Loading

0 comments on commit 7213297

Please sign in to comment.