camkes-manifest

KO | EN

gitlite — search

#c #shell #linux #java #machine-learning #web #terminal #pytorch #openai #html

camkes-manifest

(★ 26)

Top level project for CAmkES, a component platform that provides support for developing and building static seL4 systems as a collection of interacting components.

파일 탐색기

ZIP 다운로드

- - pr.yml
  - push.yml
- CODE_OF_CONDUCT.md
- CONTRIBUTING.md
- BSD-2-Clause.txt
- CC-BY-SA-4.0.txt
- snapshot-20150518171951.xml
default.xml
l4v-master.xml
master.xml
README.md
working.xml

# CDN으로 사용하기

jsDelivr

jsDelivr는 공개 GitHub 리포지토리를 별도 설정 없이 CDN으로 즉시 서빙합니다. 버전과 파일을 고르면 웹페이지에 바로 붙일 수 있는 링크와 예시 코드가 만들어집니다.

버전

파일

링크

예시

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

<!--
     Copyright 2018, Data61, CSIRO

SPDX-License-Identifier: CC-BY-SA-4.0
-->

camkes-manifest
===============
CAmkES is a component platform that provides support for developing and building static
seL4 systems as a collection of interacting components.  The resulting systems are static,
meaning that all the components and their connections (and thus all the kernel
managed resources) are defined at design time and instantiated at system initialisation time.
It is not possible to change the system (e.g., to create or destroy components or to change
the connections between components) at runtime.  This CAmkES package includes various example
systems that can be studied, and individually built and run.

For general instructions on how to use this repository, see [sel4.systems](https://docs.sel4.systems/RepoCheatsheet).

For general information about CAmkES see [the CAmkES pages on seL4.systems](https://docs.sel4.systems/projects/camkes/).

For detailed information about CAmkES see documentation in [the camkes-tool repo](https://github.com/seL4/camkes-tool/blob/master/docs/index.md).

Prerequisites, in addition to a standard build system for your target, are:
* The Haskell compiler, ghc
* Haskell libraries missingH, split and data-ordlist
* Python
* Python libraries python-tempita, pyelftools, jinja2 and ply
* which, realpath and the libxml2 utilities.

## Dependencies for verification

The toolchain can generate formal specifications and proofs about how
a CAmkES spec is mapped to seL4 objects (via capDL). To run these
proofs, checkout the `l4v-master` manifest, e.g. with:

repo init -m l4v-master.xml
    repo sync

Then enable these extra `init-build` options:

../init-build.sh [...] -DCAmkESCapDLStaticAlloc=1 -DCAmkESCapDLVerification=1

You will also need to install additional dependencies; see the
[L4.verified setup instructions](https://github.com/seL4/l4v/blob/master/README.md).

Note that the proof toolchain does not support all CAmkES features.

camkes-manifest

오너의 다른 레포

파일 탐색기

# CDN으로 사용하기

Was this content helpful?

Recent Feedback

camkes-manifest

오너의 다른 레포

파일 탐색기

# CDN으로 사용하기

Was this content helpful?

Recent Feedback

Download README