benchmarks

KO | EN

gitlite — search

#react #ai #llm #go #golang #deep-learning #docker #macos #nodejs #kubernetes #vue #security #pytorch #ios

(★ 9)

A hub for sharing ideas on planning, executing and evaluating benchmarks.

benchmarks 최신버젼 다운로드

최종 버전 다운로드 (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# Benchmarks

This repository contains benchmarks for formal co-validation of hardware and
low-level software interfaces. The source code for these benchmarks was
extracted from QEMU and Linux.

## RTC Benchmark

The __RTC__ benchmark illustrates the hardware/software interface for a
real-time clock. The focus is on Register B and the ten time/calendar and alarm
bytes:

![RTC Registers][rtc-registers]

Courtesy of [MC146818 data sheet][rtc-datasheet]

To run the experiments on the HW/SW model, execute the following command from
within the folder `sw-hw/linux/rtc_x86`:

$ ./run_expt.sh [Num of Runs] [Experiment Name] [Property No. (1 to 11)]

You can also run the experiment from propery i to j once by exectuing the 
following command within the same folder:

$ ./run_expt_all.sh [Experiment Name] [i] [j]

Use the same command in the folder `qemu-hw/rtc` to run the experiments on the
standalone HW model.

To get the total runtime and runtime spent on the decision procedure produced 
by the script run_expt.sh, run the command:

$ ./get_result.sh [(Relative) Path to the Data Folder]

Note: get_result.sh does not work with the script run_expt_all.sh

## I2C Benchmark

The __I2C__ benchmark illustrates hardware/software interface for a temperature
sensor on a serial bus. Thus, this benchmark goes beyond fixed-sized register
updates as illustrated by the following waveform:

![TMP105 I2C Write Word Protocol][tmp105-i2c-word-write]

Courtesy of [TMP105 data sheet][tmp105-datasheet]

To run the experiments on the HW/SW model, execute the following command
from within the folder `sw-hw/linux/tmp105_x86`:

$ ./run_expt.sh [Num of Runs] [Experiment Name] [Property No. (1 to 17)]

You can also run the experiment from propery i to j once by exectuing the 
following command within the same folder:

$ ./run_expt_all.sh [Experiment Name] [i] [j]

Use the same command in folder `qemu-hw/tmp105` to run experiments on the
standalone HW model (property no. 1 to 8, and 10 to 20).

To get the total runtime and runtime spent on the decision procedure produced 
by the script run_expt.sh, run the command:

$ ./get_result.sh [(Relative) Path to the Data Folder]

Note: get_result.sh does not work with the script run_expt_all.sh

## ETHOC Benchmark

The __ETHOC__ benchmark exemplifies a known concurrency bug in a NAPI-enabled
driver for an Ethernet MAC.

The concurrent interactions of software and hardware are best clarified in the
graphs showing the interleaving of software and hardware model threads. These
are available in [PNG][ethoc-prop5-msc-png] and [SVG][ethoc-prop5-msc-svg]
format (the corresponding partial orders used by CBMC are also available in
graphical form, as [SVG][ethoc-prop5-rel-svg] or [PDF][ethoc-prop5-rel-pdf]).

Summary tables and full log files of these experiments are available at
[ethoc-hw] for the hardware model, and [ethoc-sw-hw] for the combined
hardware+software implementation. These tables and results were generated using
our [benchmarking framework][cpbm]. The corresponding commands are documented in
the scripts [ethoc-hw-experiments] and [ethoc-sw-hw-experiments], which were
used to compute and generate all these results.

## Contribute Benchmarks

We welcome contributions of new benchmarks. See also our [Wiki][wiki] for
useful resources.

[rtc-registers]: https://raw.github.com/ahorn/benchmarks/master/doc/rtc/rtc_registers.jpg
[rtc-datasheet]: http://www.freescale.com/files/microcontrollers/doc/data_sheet/MC146818.pdf
[tmp105-datasheet]: http://www.ti.com/lit/ds/symlink/tmp105.pdf
[tmp105-i2c-word-write]: https://raw.github.com/ahorn/benchmarks/master/doc/i2c/tmp105-i2c-word-write.jpg
[ethoc-hw]: http://htmlpreview.github.com/?https://github.com/ahorn/benchmarks/master/doc/ethoc/ethoc-hw.web/index.html
[ethoc-sw-hw]: http://htmlpreview.github.com/?https://github.com/ahorn/benchmarks/master/doc/ethoc/ethoc-sw-hw.web/index.html
[ethoc-hw-experiments]: https://github.com/ahorn/benchmarks/blob/master/qemu-hw/ethoc/experiments.sh
[ethoc-sw-hw-experiments]: https://github.com/ahorn/benchmarks/blob/master/sw-hw/linux/ethoc/experiments.sh
[ethoc-prop5-msc-png]: https://raw.github.com/ahorn/benchmarks/master/doc/ethoc/prop5.png
[ethoc-prop5-msc-svg]: http://htmlpreview.github.com/?https://raw.github.com/ahorn/benchmarks/master/doc/ethoc/prop5.svg
[ethoc-prop5-rel-svg]: http://htmlpreview.github.com/?https://raw.github.com/ahorn/benchmarks/master/doc/ethoc/prop5-relations.svg
[ethoc-prop5-rel-pdf]: https://raw.github.com/ahorn/benchmarks/master/doc/ethoc/prop5-relations.pdf
[cpbm]: http://www.cprover.org/software/benchmarks/
[wiki]: https://github.com/ahorn/benchmarks/wiki/_pages

benchmarks

benchmarks 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

benchmarks

benchmarks 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

Download README