-
Notifications
You must be signed in to change notification settings - Fork 5
/
multi_main.camkes
129 lines (112 loc) · 4.41 KB
/
multi_main.camkes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <configurations/vm.h>
import <std_connector.camkes>;
import <global-connectors.camkes>;
import <seL4VMDTBPassthrough.idl4>;
import <FileServerInterface.camkes>;
import <FileServer/FileServer.camkes>;
import <SerialServer/SerialServer.camkes>;
import <TimeServer/TimeServer.camkes>;
import <vm-connectors.camkes>;
import <multi_devices.camkes>;
struct vswitch_mapping {
string mac_addr;
int send_id;
int recv_id;
};
component VM {
VM_INIT_DEF()
maybe uses VirtQueueDev recv1;
maybe uses VirtQueueDrv send1;
maybe uses VirtQueueDev recv2;
maybe uses VirtQueueDrv send2;
attribute vswitch_mapping vswitch_layout[] = [];
attribute string vswitch_mac_address = "";
}
assembly {
composition {
/* Boilerplate composition settings */
VM_GENERAL_COMPOSITION_DEF()
/* Other standard VM defintions (vm0, vm1, vm1) */
VM_COMPOSITION_DEF(0)
VM_COMPOSITION_DEF(1)
VM_COMPOSITION_DEF(2)
/* vm0,vm1 & vm2 serial connections */
VM_VIRTUAL_SERIAL_COMPOSITION_DEF(0,1,2)
/* vm0-[vm1,vm2] connection */
component VirtQueueInit vm1_vm0;
component VirtQueueInit vm2_vm0;
connection seL4VirtQueues vm1_vm0_conn(to vm1_vm0.init, from vm0.send1, from vm0.recv1, from vm1.send1, from vm1.recv1);
connection seL4VirtQueues vm2_vm0_conn(to vm2_vm0.init, from vm0.recv2, from vm0.send2, from vm2.recv1, from vm2.send1);
/* DTB Passthrough */
connection seL4VMDTBPassthrough vm0_dtb(from vm0.dtb_self, to vm0.dtb);
connection seL4VMDTBPassthrough vm1_dtb(from vm1.dtb_self, to vm1.dtb);
connection seL4VMDTBPassthrough vm2_dtb(from vm2.dtb_self, to vm2.dtb);
}
configuration {
VM_GENERAL_CONFIGURATION_DEF()
VM_CONFIGURATION_DEF(0)
VM_CONFIGURATION_DEF(1)
VM_CONFIGURATION_DEF(2)
VM_VIRTUAL_SERIAL_CONFIGURATION_DEF(0,1,2)
vm0.num_extra_frame_caps = 0;
vm0.extra_frame_map_address = 0;
vm0.cnode_size_bits = 18;
vm0.simple_untyped21_pool = 12;
vm0.simple_untyped12_pool = 12;
vm0.vswitch_mac_address = "02:00:00:00:AA:01";
vm0.vswitch_layout = [{"mac_addr": "02:00:00:00:AA:02", "recv_id": 0, "send_id":1},
{"mac_addr": "02:00:00:00:AA:03", "recv_id": 2, "send_id":3}];
vm1.num_extra_frame_caps = 0;
vm1.extra_frame_map_address = 0;
vm1.cnode_size_bits = 18;
vm1.simple_untyped21_pool = 12;
vm1.simple_untyped12_pool = 12;
vm1.vswitch_mac_address = "02:00:00:00:AA:02";
vm1.vswitch_layout = [{"mac_addr": "02:00:00:00:AA:01", "recv_id": 0, "send_id":1}];
vm2.num_extra_frame_caps = 0;
vm2.extra_frame_map_address = 0;
vm2.cnode_size_bits = 18;
vm2.simple_untyped21_pool = 12;
vm2.simple_untyped12_pool = 12;
vm2.vswitch_mac_address = "02:00:00:00:AA:03";
vm2.vswitch_layout = [{"mac_addr": "02:00:00:00:AA:01", "recv_id": 0, "send_id":1}];
/* VM0-VM1 virtqueue configurations */
vm0.recv1_id = 0;
vm0.recv1_attributes = "01";
vm0.recv1_shmem_size = 8192;
vm0.send1_id = 1;
vm0.send1_attributes = "10";
vm0.send1_shmem_size = 8192;
/* VM0-VM2 virtqueue configurations */
vm0.recv2_id = 2;
vm0.recv2_attributes = "20";
vm0.recv2_shmem_size = 8192;
vm0.send2_id = 3;
vm0.send2_attributes = "02";
vm0.send2_shmem_size = 8192;
/* VM1 virtqueue configurations */
vm1.recv1_id = 0;
vm1.recv1_attributes = "10";
vm1.recv1_shmem_size = 8192;
vm1.send1_id = 1;
vm1.send1_attributes = "01";
vm1.send1_shmem_size = 8192;
/* VM2 virtqueue configurations */
vm2.recv1_id = 0;
vm2.recv1_attributes = "02";
vm2.recv1_shmem_size = 8192;
vm2.send1_id = 1;
vm2.send1_attributes = "20";
vm2.send1_shmem_size = 8192;
/* Virtqueue Topology */
vm1_vm0.init_topology = [{ "drv" : "vm0.send1", "dev" : "vm1.recv1"},
{ "drv" : "vm1.send1", "dev" : "vm0.recv1"}];
vm2_vm0.init_topology = [{ "drv" : "vm0.send2", "dev" : "vm2.recv1"},
{ "drv" : "vm2.send1", "dev" : "vm0.recv2"}];
}
}