Skip to content

Commit

Permalink
add build instructions for new micro-examples
Browse files Browse the repository at this point in the history
  • Loading branch information
jasonbelt committed Nov 12, 2024
1 parent a475d0f commit a2491c9
Show file tree
Hide file tree
Showing 12 changed files with 1,022 additions and 9 deletions.
2 changes: 1 addition & 1 deletion micro-examples/microkit/aadl_port_types/data/aadl/.system
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
system_impl=top.impl
system_impl_file=event_data_1_prod_2_cons.aadl
system_impl_file=data_1_prod_2_cons.aadl
projects=.
103 changes: 103 additions & 0 deletions micro-examples/microkit/aadl_port_types/data/aadl/bin/run-hamr.cmd
Original file line number Diff line number Diff line change
@@ -0,0 +1,103 @@
::/*#! 2> /dev/null #
@ 2>/dev/null # 2>nul & echo off & goto BOF #
if [ -z ${SIREUM_HOME} ]; then #
echo "Please set SIREUM_HOME env var" #
exit -1 #
fi #
exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" #
:BOF
setlocal
if not defined SIREUM_HOME (
echo Please set SIREUM_HOME env var
exit /B -1
)
%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
exit /B %errorlevel%
::!#*/
// #Sireum

import org.sireum._

val aadlDir = Os.slashDir.up


val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")

val osate: Os.Path = Os.env("OSATE_HOME") match {
case Some(s) => Os.path(s) / (if (Os.isWin) "osate.exe" else if (Os.isLinux) "osate" else "Contents/MacOs/osate")
case _ if (Os.isWin) => sireumBin / "win" / "fmide" / "fmide.exe"
case _ if (Os.isMac) => sireumBin / "mac" / "fmide.app" / "Contents" / "MacOs" / "osate"
case _ if (Os.isLinux) => sireumBin / "linux" / "fmide" / "fmide"
case _ =>
println("Unsupported operating system")
Os.exit(1)
halt("")
}

if (!osate.exists) {
eprintln("Please install FMIDE (e.g. '$SIREUM_HOME/bin/install/fmide.cmd') or OSATE (e.g. 'sireum hamr phantom -u')")
Os.exit(1)
halt("")
}

val osireum = ISZ(osate.string, "-nosplash", "--launcher.suppressErrors", "-data", "@user.home/.sireum", "-application", "org.sireum.aadl.osate.cli")

if(Os.cliArgs.size > 1) {
eprintln("Only expecting a single argument")
Os.exit(1)
}

val platform: String =
if(Os.cliArgs.nonEmpty) Os.cliArgs(0)
else "Microkit"

val packageName = "microkit" // not used for 'microkit' platform

val excludeComponentImpl = F

// commenting out options that are not used by 'microkit' platform
var codegenArgs = ISZ("hamr", "codegen",
"--platform", platform,
//"--package-name", packageName,
//"--output-dir", (aadlDir.up / "hamr" / "slang").string,
//"--output-c-dir", (aadlDir.up / "hamr" / "c").string,
"--camkes-output-dir", (aadlDir.up / "hamr" / "microkit").string,
//"--run-transpiler",
//"--bit-width", "32",
//"--max-string-size", "256",
//"--max-array-size", "1",
"--verbose",
//"--workspace-root-dir", aadlDir.string
)

if (platform == "JVM") {
codegenArgs = codegenArgs :+ "--runtime-monitoring"
} else {
println("***********************************************************************")
println(s"Note: runtime-monitoring support is not yet avialable for ${platform}")
println("***********************************************************************")
}

if (excludeComponentImpl) {
//codegenArgs = codegenArgs :+ "--exclude-component-impl"
}

if ((aadlDir.up / "hamr" / "slang" / ".idea").exists) {
codegenArgs = codegenArgs :+ "--no-proyek-ive"
}

codegenArgs = codegenArgs :+ (aadlDir / ".system").string

val results = Os.proc(osireum ++ codegenArgs).echo.console.run()

// Running under windows results in 23 which is an indication
// a platform restart was requested. Codegen completes
// successfully and the cli app returns 0 so
// not sure why this is being issued.
if(results.exitCode == 0 || results.exitCode == 23) {
Os.exit(0)
} else {
println(results.err)
Os.exit(results.exitCode)
}
130 changes: 129 additions & 1 deletion micro-examples/microkit/aadl_port_types/data/readme.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,132 @@
|--|--|
|Threads|3|
|Ports|3|
|Connections|2|
|Connections|2|



## Codegen

1. Install [Docker Desktop](https://www.docker.com/products/docker-desktop/)

1. Clone this repo and cd into it ``INSPECTA-models``

```
git clone https://github.com/loonwerks/INSPECTA-models.git
cd INSPECTA-models
```

1. *OPTIONAL*

If you want to rerun codegen then you will need to install Sireum
and OSATE. You can do this inside or outside of the container that you'll install in the next step (the latter is probably preferable as you could then use Sireum outside of the container).

Copy/paste the following to install Sireum
```
git clone https://github.com/sireum/kekinian.git
kekinian/bin/build.cmd
```
This installs/build Sireum from source rather than via a binary distribution (which is probably the prefered method for PROVERS).
Now set ``SIREUM_HOME`` to point to where you cloned kekinian and add ``$SIREUM_HOME/bin`` to your path. E.g. for bash
```
echo "export SIREUM_HOME=$(pwd)/kekinian" >> $HOME/.bashrc
echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
source $HOME/.bashrc
```
To update Sireum in the future do the following
```
cd $SIREUM_HOME
git pull --rec
bin/build.cmd
```
Now install OSATE and the Sireum OSATE plugins into your current directory (or wherever as indicated via the ``-o`` option). For Windows/Linux
```
sireum hamr phantom -u -v -o $(pwd)/osate
```
or for Mac copy/paste
```
sireum hamr phantom -u -v -o $(pwd)/osate.app
```
Now set ``OSATE_HOME`` to point to where you installed Osate
```
echo "export OSATE_HOME=$(pwd)/osate" >> $HOME/.bashrc
source $HOME/.bashrc
```
1. Download and run the CAmkES docker container, mounting the ``INSPECTA-models`` directory into it
```
docker run -it -w /root -v $(pwd):/root/INSPECTA-models jasonbelt/microkit_domain_scheduling
```
This container includes customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests
- [microkit #175](https://github.com/seL4/microkit/pull/175)
- [seL4 #1308](https://github.com/seL4/seL4/pull/1308)
1. *OPTIONAL* Rerun codegen
Launch the Slash script [micro-examples/microkit/aadl_port_types/data/aadl/bin/run-hamr.cmd](aadl/bin/run-hamr.cmd) from the command line.
```
micro-examples/microkit/aadl_port_types/data/aadl/bin/run-hamr.cmd
```
1. Build and simulate the image
Inside the container do the following
```
export MICROKIT_BOARD=qemu_virt_aarch64
export MICROKIT_SDK=/root/microkit/release/microkit-sdk-1.4.1-dev.14+cf88629
cd $HOME/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/hamr/microkit
make qemu
```
Type ``CTRL-a x`` to exit the QEMU simulation
You should get output similar to
```
Booting all finished, dropped to user space
MON|INFO: Microkit Bootstrap
MON|INFO: bootinfo untyped list matches expected list
MON|INFO: Number of bootstrap invocations: 0x00000009
MON|INFO: Number of system invocations: 0x000000c5
MON|INFO: completed bootstrap invocations
MON|INFO: completed system invocations
consumer_p_p_con: I'm periodic
consumer_p_s_con: I'm sporadic so you'll never hear from me again :(
producer_p_p_pro: I'm periodic, initialized outgoing data port
consumer_p_p_con: retrieved 0 which is fresh
------
producer_p_p_pro: nothing sent
consumer_p_p_con: retrieved 0 which is stale
------
producer_p_p_pro: sent 2
consumer_p_p_con: retrieved 2 which is fresh
------
producer_p_p_pro: nothing sent
consumer_p_p_con: retrieved 2 which is stale
------
producer_p_p_pro: sent 4
consumer_p_p_con: retrieved 4 which is fresh
------
producer_p_p_pro: nothing sent
consumer_p_p_con: retrieved 4 which is stale
------
producer_p_p_pro: sent 6
consumer_p_p_con: retrieved 6 which is fresh
------
producer_p_p_pro: nothing sent
consumer_p_p_con: retrieved 6 which is stale
```
2 changes: 1 addition & 1 deletion micro-examples/microkit/aadl_port_types/event/aadl/.system
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
system_impl=top.impl
system_impl_file=event_data_1_prod_2_cons.aadl
system_impl_file=event_2_prod_2_cons.aadl
projects=.
103 changes: 103 additions & 0 deletions micro-examples/microkit/aadl_port_types/event/aadl/bin/run-hamr.cmd
Original file line number Diff line number Diff line change
@@ -0,0 +1,103 @@
::/*#! 2> /dev/null #
@ 2>/dev/null # 2>nul & echo off & goto BOF #
if [ -z ${SIREUM_HOME} ]; then #
echo "Please set SIREUM_HOME env var" #
exit -1 #
fi #
exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" #
:BOF
setlocal
if not defined SIREUM_HOME (
echo Please set SIREUM_HOME env var
exit /B -1
)
%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
exit /B %errorlevel%
::!#*/
// #Sireum

import org.sireum._

val aadlDir = Os.slashDir.up


val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")

val osate: Os.Path = Os.env("OSATE_HOME") match {
case Some(s) => Os.path(s) / (if (Os.isWin) "osate.exe" else if (Os.isLinux) "osate" else "Contents/MacOs/osate")
case _ if (Os.isWin) => sireumBin / "win" / "fmide" / "fmide.exe"
case _ if (Os.isMac) => sireumBin / "mac" / "fmide.app" / "Contents" / "MacOs" / "osate"
case _ if (Os.isLinux) => sireumBin / "linux" / "fmide" / "fmide"
case _ =>
println("Unsupported operating system")
Os.exit(1)
halt("")
}

if (!osate.exists) {
eprintln("Please install FMIDE (e.g. '$SIREUM_HOME/bin/install/fmide.cmd') or OSATE (e.g. 'sireum hamr phantom -u')")
Os.exit(1)
halt("")
}

val osireum = ISZ(osate.string, "-nosplash", "--launcher.suppressErrors", "-data", "@user.home/.sireum", "-application", "org.sireum.aadl.osate.cli")

if(Os.cliArgs.size > 1) {
eprintln("Only expecting a single argument")
Os.exit(1)
}

val platform: String =
if(Os.cliArgs.nonEmpty) Os.cliArgs(0)
else "Microkit"

val packageName = "microkit" // not used for 'microkit' platform

val excludeComponentImpl = F

// commenting out options that are not used by 'microkit' platform
var codegenArgs = ISZ("hamr", "codegen",
"--platform", platform,
//"--package-name", packageName,
//"--output-dir", (aadlDir.up / "hamr" / "slang").string,
//"--output-c-dir", (aadlDir.up / "hamr" / "c").string,
"--camkes-output-dir", (aadlDir.up / "hamr" / "microkit").string,
//"--run-transpiler",
//"--bit-width", "32",
//"--max-string-size", "256",
//"--max-array-size", "1",
"--verbose",
//"--workspace-root-dir", aadlDir.string
)

if (platform == "JVM") {
codegenArgs = codegenArgs :+ "--runtime-monitoring"
} else {
println("***********************************************************************")
println(s"Note: runtime-monitoring support is not yet avialable for ${platform}")
println("***********************************************************************")
}

if (excludeComponentImpl) {
//codegenArgs = codegenArgs :+ "--exclude-component-impl"
}

if ((aadlDir.up / "hamr" / "slang" / ".idea").exists) {
codegenArgs = codegenArgs :+ "--no-proyek-ive"
}

codegenArgs = codegenArgs :+ (aadlDir / ".system").string

val results = Os.proc(osireum ++ codegenArgs).echo.console.run()

// Running under windows results in 23 which is an indication
// a platform restart was requested. Codegen completes
// successfully and the cli app returns 0 so
// not sure why this is being issued.
if(results.exitCode == 0 || results.exitCode == 23) {
Os.exit(0)
} else {
println(results.err)
Os.exit(results.exitCode)
}
Loading

0 comments on commit a2491c9

Please sign in to comment.