Skip to content

Commit

Permalink
update sireum version
Browse files Browse the repository at this point in the history
  • Loading branch information
@jasonbelt
jasonbelt committed May 17, 2024
1 parent 9d66504 commit 566009a
Show file tree
Hide file tree
Showing 8 changed files with 17 additions and 221 deletions.
1 change: 1 addition & 0 deletions basic/test_data_port_periodic_domains/microkit/periodic_dispatcher.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ void notified(microkit_channel channel) {
switch(channel) {
case PORT_FROM_END_OF_SCHEDULE_PING:
//printf("%s: Received ping\n", ID);
printf("----------------------\n");
pingComponents();
break;
}
Expand Down
1 change: 0 additions & 1 deletion basic/test_data_port_periodic_domains/microkit/producer.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ void notified(microkit_channel channel) {

*((int*) to_consumer_vaddr) = ++counter;

printf("---------------------------\n");
printf("%s: Sent %i \n", ID, counter);

break;
Expand Down
11 changes: 11 additions & 0 deletions basic/test_data_port_periodic_domains/microkit/questions.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
- How do specify a fixed static schedule?

- Is notify called multiple times per dispatch when 2+ events are received? Can one notification per dispatch be enforced?

- Can notifications be dropped (i.e. by microkit)?

- Is there anyway to do fanouts (i.e. not just different channels from the sender)?

- Time servers? e.g. ODROID C4 timer [https://github.com/seL4/microkit/tree/main/example/odroidc4/timer](https://github.com/seL4/microkit/tree/main/example/odroidc4/timer)

- Can components flush their budgets (UNSW)
2 changes: 1 addition & 1 deletion basic/test_data_port_periodic_domains/readme.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ repository.

Copy/paste the following into the container to install Sireum
```
(DIR=$HOME/Sireum && export SIREUM_V=4.20240508.f1c262c && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
(DIR=$HOME/Sireum && export SIREUM_V=4.20240517.2ba56a5 && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
echo "export SIREUM_HOME=$HOME/Sireum" >> $HOME/.bashrc
echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
source $HOME/.bashrc
Expand Down
2 changes: 1 addition & 1 deletion basic/test_event_data_port_periodic_domains/readme.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ repository.

Copy/paste the following into the container to install Sireum
```
(DIR=$HOME/Sireum && export SIREUM_V=4.20240508.f1c262c && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
(DIR=$HOME/Sireum && export SIREUM_V=4.20240517.2ba56a5 && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
echo "export SIREUM_HOME=$HOME/Sireum" >> $HOME/.bashrc
echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
source $HOME/.bashrc
Expand Down
2 changes: 1 addition & 1 deletion basic/test_event_port_periodic_domains/readme.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ repository.

Copy/paste the following into the container to install Sireum
```
(DIR=$HOME/Sireum && export SIREUM_V=4.20240508.f1c262c && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
(DIR=$HOME/Sireum && export SIREUM_V=4.20240517.2ba56a5 && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
echo "export SIREUM_HOME=$HOME/Sireum" >> $HOME/.bashrc
echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
source $HOME/.bashrc
Expand Down
217 changes: 1 addition & 216 deletions bin/readme-gen/src/main/report/Report.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -670,168 +670,6 @@ object Report {
else r
}

def processResults(csv: Os.Path): HashSMap[String, ST] = {

val rawlines = csv.readLines
assert(rawlines(0) == "entrypoint,cliTime,logikaTime,processBegin,processCheck,vcsNum,vcsTime,satNum,satTime,timeStamp,kekikianBuild,timeout,rlimit,par,par-branch,par-branch-mode,System Version,Computer Name,Model Identifier,Processor,Memory")
val lines: ISZ[ISZ[String]] = for (l <- ops.ISZOps(rawlines).drop(1)) yield ops.StringOps(l).split(c => c == ',')

var entrypoints: Set[String] = Set.empty
for (l <- lines) {
entrypoints = entrypoints + l(0)
}
var ret = HashSMap.empty[String, ST]
for (entryPoint <- entrypoints.elements) {
val entries = ops.ISZOps(lines).filter(p => p(0) == entryPoint)
val cliTime = collect(1, entries)
val logikaTime = collect(2, entries)
val processBegin = collect(3, entries)
val processCheck = collect(4, entries)
val vcsNum = collect(5, entries)
allSame(5, entries)
val vcsTime = collect(6, entries)
val satNum = collect(7, entries)
allSame(7, entries)
val satTime = collect(8, entries)

val ttime = formatTime(logikaTime)
val itctime = formatTime(processBegin - processCheck)
val vtime = formatTime(processCheck)


ret = ret + entryPoint ~> st"|$vcsNum|$satNum|$ttime|$itctime|$vtime|"
}
return ret
}

// NOTE: ignore tipe warning that SymbolTable cannot be resolved as the source
// for that is in the jitpack jar file and thus not accessible to tipe
def genLogikaSection(project: ReadmeGen.Project, table: SymbolTable): ReportLevel = {
var subLevels: ISZ[ReportBlock] = ISZ()
for (t <- table.getThreads()) {
val cimplname: String = sanitize(splitClassifier(t)._2)
val sp = st"${(ops.ISZOps(t.path).drop(1), "_")}".render
val fnamePrefix: String = s"${cimplname}_${sp}"
val scalaFilename = s"${fnamePrefix}.scala"

val csvFilename = s".${scalaFilename}.csv"

val componentDir = Os.path(project.configs(0).outputDir.get) / "src" / "main" / "component" / project.configs(0).packageName.get
val csvFile = Os.Path.walk(componentDir, T, F, p => p.name == csvFilename)
val scalaFile = Os.Path.walk(componentDir, T, F, p => p.name == scalaFilename)(0)

if (csvFile.nonEmpty) {
val tag = createTag(s"logika-${fnamePrefix}")
var entries: ISZ[ST] = ISZ()
for (r <- processResults(csvFile(0)).entries) {
val lineNum = findMethod(r._1, scalaFile)
val elink = st"[${r._1}](${project.projectRootDir.relativize(scalaFile)}#L${lineNum})"
entries = entries :+ st"|${elink}${r._2}"
}
val table =
st"""
|**${t.identifier}**
|
|Raw Data: [csv](${project.projectRootDir.relativize(csvFile(0))})
|
|EntryPoint|VC|SAT|TTime|ITCTime|VTime|
||:--|:--|:--|:--|:--|:--|
|${(entries, "\n")}"""

subLevels = subLevels :+ ReportBlock(
tag = tag,
content = Some(table)
) /*
subLevels = subLevels :+ Level(
tag = tag,
title = Some(st"${t.identifier}"),
description = None(),
content = ISZ(Block(s"${tag}-table", Some(table))),
subLevels = ISZ()
)*/
}
}

val results = ReportLevel(
tag = createTag("logiak-results"),
title = Some(st"Results"),
description = None(),
content = subLevels,
subLevels = ISZ()
)
val slashScript = repoRoot / "bin" / "report-logika.cmd"
val relSlashScript = project.projectRootDir.relativize(slashScript)

val howToRun = ReportLevel(
tag = createTag("how-to-run"),
title = Some(st"How to replicate"),
description = Some(
st"""To run the experiments, first install Sireum Kekinian (optionally choosing the
|commit tip used for the experiments, ie. [843ede1](https://github.com/sireum/kekinian/tree/843ede1120e6e75fde089db0928ab66a3c9a3e73))
|
|```
|git clone --rec https://github.com/sireum/kekinian.git
|cd kekinian
|git checkout 843ede1
|git pull --rec
|bin/build.cmd
|
|export SIREUM_HOME=$$(pwd)
|export PATH=$$SIREUM_HOME/bin:$$PATH
|```
|
|Then run the following Slash script specifying the number of number of times to rerun Logika
|on each entrypoint: [${relSlashScript}](${relSlashScript})
|
|```
|${relSlashScript} run 25
|```
|
|The results will be appended to the csv file corresponding to the component
|being evaluated. The line ``val projects: Map[String, Project] = Map.empty + isolette + rts + tcP + tcS``
|in the script can be modified if you want to run a subset of the projects"""),
content = ISZ(), subLevels = ISZ()
)

return ReportLevel(
tag = createTag("logika"),
title = Some(st"Logika"),
description = Some(
st"""The following reports the experimental data obtained by running Logika
|only on the component entrypoints that require verification (e.g. TempControl's
|Fan component was excluded as it does not contain GUMBO contracts and does not
|use datatypes that have invariants). Logika was configured with a 2 second
|validity checking timeout, a 500 millisecond satisfiability checking timeout, a
|SMT2 resource limit of 2,000,000, and with full parallelization optimizations
|enabled. The SMT2 solvers used include CVC4 1.8, CVC5 1.0.5, and Z3 4.12.2. The
|**VC** and **SAT** columns report the number of verification and
|satisfiability conditions that were checked, respectively. The time values
|reported in the final three columns are the averages obtained after re-running
|Logika 25 times for each entrypoint on an M1 Mac Mini with 8 cores and 16 GB of
|RAM. **TTime** gives the total number of seconds it took to run Logika
|from the command line on the Slang project containing the entrypoint (i.e. it
|includes the verification time along with the time required for parsing, type
|checking, etc.).
|
|One optimization technique related to using Logika from within IVE that can be
|measured via our experimental setup is Sireum's incremental type checking. For
|example, if Logika was run on the Isolette MA component's initialize entrypoint
|from within IVE using an identical configuration as was done for the experiments
|then it will take on average 2.482 seconds to verify, assuming Logika had not
|previously been invoked. If a change was then made to MA's source code before
|re-running Logika on the timeTriggered entrypoint then Sireum's incremental type
|checking will only need to recheck MA (and any of its dependents) resulting in
|an average delay of only 0.214 seconds before verification can proceed. The
|results of these optimizations are reported in the Incremental-Type Checking
|column (**ITCTime**). The time required to actually verify an entrypoint with
|a clean cache is reported in the Verification-Time column (**VTime**) so
|incremental type checking for this example would save 2.268 seconds (2.482 -
|0.214) on average."""),
content = ISZ(),
subLevels = ISZ(results, howToRun)
)
}

def genArchitectureSection(project: Project, table: SymbolTable): ReportLevel = {

var blocks: ISZ[ReportBlock] = ISZ()
Expand Down Expand Up @@ -945,59 +783,6 @@ object Report {
)
}

/*
def genBehaviorCodeSection(project: ReadmeGen.Project, table: SymbolTable): ReportLevel = {
var threads: ISZ[ReportBlock] = ISZ()
for (thread <- table.getThreads()) {
val tpath = st"${(ops.ISZOps(thread.path).drop(1), "_")}".render
val (behavior, gumbox) = findBehaviorCode(tpath, project)
val gumboxOpt: Option[ST] = if (gumbox.nonEmpty)
Some(st"<br>[GumboX](${project.projectRootDir.relativize(gumbox.get)})")
else None()
threads = threads :+
ReportBlock(
tag = createTag(s"slang-code-${thread.identifier}-$tnick"),
content = Some(
st"""[${tnick}](${project.projectRootDir.relativize(behavior.get)})
|${gumboxOpt}""")
)
}
val description = st"""The following items link to the Slang source code for the application logic of each thread.
|In the HAMR development workflow, skeletons for these files are automatically created,
|along with APIs for communicating over model-declared ports in the component type.
|GUMBO component contracts in the AADL model are automatically translated to Slang/Logika
|contracts and included in the generated skeletons. Then, the application developer uses a
|conventional development approach for coding the application logic in Slang
|(C workflows are also supported). Logika can be applied to verify that the user's
|application code conforms to the generated Logika contracts (which are derived
|automatically from model-level GUMBO contracts). The HAMR build framework will integrate
|the user-code application logic for each component (below) with auto-generated threading
|and communication infrastructure code, along with HAMR's implementation of AADL run-time
|(based on AADL's standardized Run-Time Services). Note that HAMR is smart enough to
|accommodate changes to model-level interface declarations (ports, etc.) as well as changes
|to GUMBO contracts -- user code will not be clobbered when the model is changed and HAMR
|code generation is rerun. Instead, HAMR uses specially designed delimiters in the
|application code files to, e.g., re-weave updated contracts into the application code.
|
|Executable Slang versions of the GUMBO contracts (referred to as "GUMBOX" contracts)
|are also automatically generated in the code generation process. These executable
|contracts are automatically integrated into the unit testing process: appropriate
|portions of the executable contracts are invoked in the pre-state and the post-state
|of a thread dispatch to dynamically check that the thread's behavior for that particular
|dispatch conforms to the model-level GUMBO contracts."""
return ReportLevel(
tag = createTag("behavior-code"),
title = Some(st"Behavior Code"),
description = Some(description),
content = threads,
subLevels = ISZ()
)
}
*/

def genSetup(): ReportLevel = {
val setup = ReportBlock(
tag = createTag("setup-block"),
Expand Down Expand Up @@ -1050,7 +835,7 @@ object Report {
|
| Copy/paste the following into the container to install Sireum
| ```
| (DIR=$$HOME/Sireum && export SIREUM_V=4.20240508.f1c262c && rm -fR $$DIR && mkdir -p $$DIR/bin && cd $$DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$$SIREUM_V/bin/init.sh && bash init.sh)
| (DIR=$$HOME/Sireum && export SIREUM_V=4.20240517.2ba56a5 && rm -fR $$DIR && mkdir -p $$DIR/bin && cd $$DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$$SIREUM_V/bin/init.sh && bash init.sh)
| echo "export SIREUM_HOME=$$HOME/Sireum" >> $$HOME/.bashrc
| echo "export PATH=\$$SIREUM_HOME/bin:\$$PATH" >> $$HOME/.bashrc
| source $$HOME/.bashrc
Expand Down
2 changes: 1 addition & 1 deletion vm/test_event_data_port_periodic_domains_VM/receiver_vm/readme.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ repository.

Copy/paste the following into the container to install Sireum
```
(DIR=$HOME/Sireum && export SIREUM_V=4.20240508.f1c262c && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
(DIR=$HOME/Sireum && export SIREUM_V=4.20240517.2ba56a5 && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
echo "export SIREUM_HOME=$HOME/Sireum" >> $HOME/.bashrc
echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
source $HOME/.bashrc
Expand Down

0 comments on commit 566009a

Please sign in to comment.