- Devel - lists.sel4.systems

Building seL4test x86_64 on Debian with the Docker image
by Jacob Yu 05 Nov '19

05 Nov '19

Hi I am building "seL4test" using the Docker image on Ubuntu 18.04.3 LTS, a 64-bit system. After entering "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" in a build directory within Docker it complained "Could NOT find NANOPB (missing: PROTOBUF_PROTOC_EXECUTABLE)". I wonder should I manually download and install protocol buffer compiler, protoc? Please advise. Thank for your help. Jacob =============================================== loading initial cache file /host/projects/sel4test/settings.cmake correct_platform_strings: Attempting to correct PLATFORM: x86_64 to new valid KernelPlatform: pc99 KernelSel4Arch: x86_64 -- Found seL4: /host/kernel -- The C compiler identification is GNU 6.5.0 -- The CXX compiler identification is GNU 6.5.0 -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- Found elfloader-tool: /host/tools/seL4/elfloader-tool -- Found musllibc: /host/projects/musllibc -- Found util_libs: /host/projects/util_libs -- Found seL4_libs: /host/projects/seL4_libs -- Found sel4_projects_libs: /host/projects/sel4_projects_libs -- Found sel4runtime: /host/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- Found PythonInterp: /usr/bin/python (found version "2.7.15") -- Could NOT find NANOPB (missing: PROTOBUF_PROTOC_EXECUTABLE) -- CPIO test cpio_reproducible_flag PASSED -- Configuring done -- Generating done -- Build files have been written to: /host/build-x86

2 2

Re: [seL4] Devel Digest, Vol 65, Issue 24
by Mcleod, Kent (Data61, Kensington NSW) 04 Nov '19

04 Nov '19

> abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world > loading initial cache file ../settings.cmake > CMake Error: Error: generator : Ninja > Does not match the generator used previously: Unix Makefiles > Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. These errors indicate that CMake already believes a project has been created in the target directory and that this project was a Makefile based project. Is there any CMakeCache.txt files located anywhere in the project structure that may be causing CMake to get confused? Otherwise you could reinitialise the tutorial project and try initialising hello-world again and that would also fix your problem.

1 0

Re: [seL4] Devel Digest, Vol 65, Issue 24
by abdi mahmud haji 31 Oct '19

31 Oct '19

i am working on sel4-tutorials for the first time .i setup my machine accordingly and then when i trying to generate the tutorials like this "./init --tut hello-world" i keep getting an error message and dont know what to do or how to fix it . the error was like bellowing =================================================== abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world loading initial cache file ../settings.cmake CMake Error: Error: generator : Ninja Does not match the generator used previously: Unix Makefiles Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 774, in __init__ self.wait() File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /home/abdi/.local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world82varrcf -C ../settings.cmake .. STDOUT: STDERR: ====================================================================== is there someone who suggests what i should do please. thanks On Sun, Oct 27, 2019 at 4:00 AM <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: releasing confidentiality > (Heiser, Gernot (Data61, Kensington NSW)) > 2. Fwd: port sel4 to RK3308(quad cortex-a35) (Yun Zhou) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 26 Oct 2019 03:07:23 +0000 > From: "Heiser, Gernot (Data61, Kensington NSW)" > <Gernot.Heiser(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] releasing confidentiality > Message-ID: <5FEA58C5-9011-49B7-9790-28B4B54849EF(a)data61.csiro.au> > Content-Type: text/plain; charset="utf-8" > > On 26 Oct 2019, at 08:00, Michael Neises <neisesmichael(a)gmail.com> wrote: > > > > Hi, > > > > I know that seL4 provides confidentiality, which is described as a > property that "means that data cannot be read without permission." Given > this wording, I wonder if it is not possible to revoke those permissions in > certain cases. In particular, I would like for one camkes component to be > able to perform runtime measurements, such as heap analysis, on another > component. Or even better, I would like for a component to be able to > perform runtime measurements on a program running within the camkes linux > vm. Is such a feat possible? > > Hi Michael > > seL4’s confidentiality (and other security) enforcement means that the > kernel guarantees that you can only access objects to which you have been > given explicit permission (in the form of a capability). How those > permissions are allocated is a matter of policy, the kernel doesn’t care, > it only enforces. > > In particular, it is totally possible in seL4 to give one component access > to another component’s address space, that’s for the user-level policy > framework to decide. > > Whether the present CAmkES framework supports this is a different > question, which I’ll leave to someone who’s more up to date with CAmkES > details. > > Gernot > > > ------------------------------ > > Message: 2 > Date: Sat, 26 Oct 2019 10:35:50 +0800 > From: Yun Zhou <shiny725829(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Fwd: port sel4 to RK3308(quad cortex-a35) > Message-ID: > <CAHNKqcxb7ws3MD=- > nwJka6HKEcA4hXZipJv0vdsStetJjxP-yg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > ---------- Forwarded message --------- > 发件人： Yun Zhou <shiny725829(a)gmail.com> > Date: 2019年10月25日周五下午9:52 > Subject: port sel4 to RK3308(quad cortex-a35) > To: <devel-owner(a)sel4.systems> > > > Dear sel4 Experts > How are you > I found some information about sel4, and sel4 is great microkernel OS, i > want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal > processing. Form the Tutorials I found sel4 just support cortex-a53, I > would like to ask does sel4 support cortex-a35 SMP mode. and because our > application is real time audio processing so system delay must lower than > 3ms and hard real-time determinism. > Will sel4 support real-time signal processing? > Looking forward to your reply > > Thanks &Kind regards > Yun >

1 0

The seL4 Foundation is coming!
by Heiser, Gernot (Data61, Kensington NSW) 25 Oct '19

25 Oct '19

Re-post from announce(a)sel4.systems<mailto:announce@sel4.systems> regarding the seL4 Foundation. We’ll start recruiting members soon. Gernot Begin forwarded message: From: Announcements about seL4 -- low volume list <announce(a)sel4.systems<mailto:announce@sel4.systems>> Subject: [seL4 Announce] The seL4 Foundation is coming! Date: 25 October 2019 at 17:09:30 AEDT To: "announce(a)sel4.systems<mailto:announce@sel4.systems>" <announce(a)sel4.systems<mailto:announce@sel4.systems>> Reply-To: <announce(a)sel4.systems<mailto:announce@sel4.systems>> Dear seL4 community, With great excitement we announce that we are in the process of setting up an seL4 Foundation, similar to foundations for other open-source projects, such as Linux and RISC-V. This will form an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. This was originally announced at the seL4 Summit in the US last month. I apologise for the delay in this posting (side-tracked with various issues). Gernot on behalf of the Trustworthy Systems team _______________________________________________ Announce mailing list Announce(a)sel4.systems<mailto:Announce@sel4.systems> https://sel4.systems/lists/listinfo/announce

1 0

Upcoming release planned
by Mcleod, Kent (Data61, Kensington NSW) 23 Oct '19

23 Oct '19

Hi all, I'm announcing that we are planning a new versioned release of seL4, capDL and CAmkES in about 3 weeks - around 11 November. We want to provide an opportunity for people to report issues or provide patches that can be fixed/incorporated for the versioned release. The last versioned release occurred almost 12 months ago and we plan on returning to a shorter release cycle of several weeks per cycle. Feel free to raise new issues across our GitHub repositories and we will also try to address any currently outstanding issues that have been neglected. Here is a highlight list of what changes are going to be in the upcoming versioned release: ## seL4 - Add GrantReply access right for endpoint capabilities. `seL4_Call` is permitted on endpoints with either the Grant or the GrantReply access rights. Capabilities can only be transferred in a reply message if receiver's endpoint capability has the Grant right. The GrantReply access right allows endpoints to be configured for two-way communication without also providing the right to transfer authority via capability transfer. - Merging of the mixed-criticality scheduling (MCS) branch into master. Previously the MCS branch only received versioned releases. Merging it into master under a build configuration (KernelIsMCS) makes it easier to keep up to date with changes to master and other tooling/libraries in-between versioned releases. Verification work is still on-going. - Continued development of the newly added RISC-V platform to support in-progress verification. - Auto-generation of Arm and RISC-V kernel platform definitions from a provided devicetree as well as support for passing a devicetree to the root task via the seL4_BootInfo structure. Interrupt controllers, timers and other devices required by the kernel can also be selected in the devicetree provided that the kernel already has a compatible driver. - Support for AArch64 hypervisors is in active development with initial support for Cortex-A53 and Cortex-A57 cores - De-duplicating kernel platform configurations and code in order to reduce the effort required to support additional platforms. - New platforms added: BeagleBone Blue, Hardkernel ODROID-C2, Freescale i.MX8M, i.MX8M Mini, Arm FVP (based on foundation-v8-gicv3.dts), QEMU ARM virt platform (with 3 CPUs: cortex-A15, cortex-A53 and cortex-A57) and possibly PINE64 ROCKPro64. - Implement RFC-3: Cross-platform thread-local storage (TLS) support. https://sel4.atlassian.net/browse/RFC-3. This provides a way for a thread to access or modify a thread-specific pointer without requiring a capability to itself. On architectures that don't provide unprivileged write access to this pointer a new syscall `seL4_SetTLSBase` is added that performs this operation. The kernel no longer reserves a register for holding a thread's IPC buffer and it is the thread's responsibility for managing this. `libsel4` declares a pointer to a thread's IPC buffer using a `__thread` keyword and a new user-level library `sel4runtime` can be used to provide a minimal supporting runtime. Additionally, the IPC buffer's userData field is no longer used for holding a pointer to the IPC buffer. - Better SMP Arm IRQ handling: Support is added for creating IRQ handler capabilities for core-local interrupts (PPIs) for each core and for also specifying a target core for global interrupts (SPIs) via the new invocation `IRQControl_GetTriggerCore`. - Merge ARCH_Page_Remap functionality into ARCH_Page_Map. Remap was used for updating the mapping attributes of a page without changing its virtual address. Now ARCH_Page_Map can be performed on an existing mapping to achieve the same result. The ARCH_Page_Remap invocation has been removed from all configurations. - Support for compiling the kernel with Clang. For a more complete list see the CHANGES file in the seL4 repository. ## CAmkES - Support for the new seL4 Endpoint GrantReply access right for CAmkES connector types. This allows multi-sender/single-receiver connectors such as `seL4RPCCall` that don't also provide the ability for arbitrary capability transfer from sender to receiver. Previously the `seL4RPC` connector was used instead of `seL4RPCCall` to create an Endpoint without a Grant right. This used a combination of `seL4_Send` and `seL4_Wait` to communicate without the ability for capability transfer, however this only supports a single sender and single receiver. - Better support for configuring components with a provided devicetree. This support includes adding a seL4DTBHardware connector that can be used instead of seL4HardwareMMIO and seL4HardwareInterrupt and can be used to extract IRQs and MMIO register information out of the devicetree node rather than specifying the info directly. This connector can also be used to access a devicetree within a component at for querying further device information. There is also a connector seL4VMDTBPassthrough that can be used for specifying devices to pass through to a `camkes-arm-vm` VM component. - CapDL Refinement framework. These are generated Isabelle proof scripts to prove that the generated capDL respects the isolation properties expected from its CAmkES system specification. Only the AARCH32 platform is supported. The generated capDL is a specification of seL4 objects and capabilities that will implement the CAmkES system specification. This specification is then given to a system initialiser to create the objects and capabilities and load the system. - Support for RISC-V systems. ## capDL capDL refers to the capability distribution language and tools contained in https://github.com/seL4/capdl. CAmkES uses these tools for generating a capDL specification and then uses the `capdl-loader-app` as it's seL4 root task for initialising the system. As we are in the process of developing additional loaders we are going to start providing versioned releases of the capDL set of tools. Changes since the last seL4 release: - Support for the new seL4 Endpoint GrantReply access rights in the CapDL spec. Endpoint capabilities in the capDL spec can now have Read, Write, Grant and GrantReply rights. - Static Untyped allocation of spec objects. This is support for performing offline pre-allocation of spec objects to the Untyped objects that are expected to be provided in the seL4_BootInfo by the kernel. Having a static allocation of spec objects to Untypeds allows for more simple loaders that do not have to perform resource allocation during initialisation. This feature is optional and a spec is still valid if objects aren't allocated from Untyped objects. - Support for loading RISC-V systems.

1 0

CAmkES languages
by Michael Neises 21 Oct '19

21 Oct '19

Hi, I have an application written in CakeML that I would like to include in a CAmkES component, but all the documentation I can find only uses C code. Is it possible to use a non-C language as source for a CAmkES component? If so, how can I accomplish this? Best, Michael Neises

2 1

Zynq UltraScale+ locks up after hours running
by Leonid Meyerovich 05 Oct '19

05 Oct '19

Hello, We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102 board). The implementation includes multiple processes, hypervisor and virtual machine running on dedicated core. After several hours running (it could be 2 or even 8 hours) the whole microkernel locks up. After some investigation I have found that no interrupts generated anymore - at least there is no interrupts coming to ISR. Inside ISR I have monitored PL2 Physical Timer Control register, which feeds a scheduler and didn't find any problems - it stays enabled and not masked. I will appreciate any idea/direction for approaching this problem. Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

5 24

Re: [seL4] [Non-DoD Source] Devel Digest, Vol 65, Issue 5
by Seeberger, John T CIV USN NAS PAX MD (USA) 05 Oct '19

05 Oct '19

I have noticed this also. Thad ________________________________________ From: Devel [devel-bounces(a)sel4.systems] on behalf of devel-request(a)sel4.systems [devel-request(a)sel4.systems] Sent: Thursday, October 03, 2019 8:24 AM To: devel(a)sel4.systems Subject: [Non-DoD Source] Devel Digest, Vol 65, Issue 5 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Zynq UltraScale+ locks up after hours running (Shen, Yanyan (Data61, Kensington NSW)) 2. Re: How to use sel4runtime (Millar, Curtis (Data61, Kensington NSW)) 3. Re: Zynq UltraScale+ locks up after hours running (Leonid Meyerovich) ---------------------------------------------------------------------- Message: 1 Date: Thu, 3 Oct 2019 06:43:52 +0000 From: "Shen, Yanyan (Data61, Kensington NSW)" <Yanyan.Shen(a)data61.csiro.au> To: "lmeyerovich(a)i-a-i.com" <lmeyerovich(a)i-a-i.com>, "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running Message-ID: <78ebf24ad9274ca75e18b5fca8575a09bc423b82.camel(a)data61.csiro.au> Content-Type: text/plain; charset="utf-8" Hi Leonid, Could you provide a bit more about your software configuration? For instance, do you have multiple VMs running on dedicated hardware cores? How are the VM and processes configured? Also, you mean there were no interrupts at all on all the four cores? Regards, Yanyan On Wed, 2019-10-02 at 16:01 +0000, Leonid Meyerovich wrote: > Hello, > > We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102 > board). The implementation includes multiple processes, hypervisor > and virtual machine running on dedicated core. After several hours > running (it could be 2 or even 8 hours) the whole microkernel locks > up. After some investigation I have found that no interrupts > generated anymore - at least there is no interrupts coming to ISR. > Inside ISR I have monitored PL2 Physical Timer Control register, > which feeds a scheduler and didn't find any problems - it stays > enabled and not masked. > > I will appreciate any idea/direction for approaching this problem. > > Thank you, > > Leonid > > > > > This message and all attachments are PRIVATE, and contain information > that is PROPRIETARY to Intelligent Automation, Inc. You are not > authorized to transmit or otherwise disclose this message or any > attachments to any third party whatsoever without the express written > consent of Intelligent Automation, Inc. If you received this message > in error or you are not willing to view this message or any > attachments on a confidential basis, please immediately delete this > email and any attachments and notify Intelligent Automation, Inc. > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel ------------------------------ Message: 2 Date: Thu, 3 Oct 2019 07:04:41 +0000 From: "Millar, Curtis (Data61, Kensington NSW)" <Curtis.Millar(a)data61.csiro.au> To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How to use sel4runtime Message-ID: <ad55f3a5de7838e0f9d16a94905647a0ead42249.camel(a)data61.csiro.au> Content-Type: text/plain; charset="utf-8" Hi Baltazar, > Another (less exclusively RISC-V related, though I am targeting RISC-V > still) question - I've been trying to figure out the sel4runtime repo, > but I'm a bit confused on how to set it up. Specifically: > > * How much of a "minimal seL4 environment" do I need to initialize > first? The sel4runtime is a minimal C runtime specifically for seL4. It handles the initialization of all applications (root servers and System-V ELF processes) on an seL4 system. A minimal project will require a repo project containing seL4, seL4_tools, musl, and sel4runtime (along with a root task application). sel4runtime is then used as the C runtime for all applications built in the project and is responsible for providing the entrypoints and calling into the main function. > * Do does my program with main() also need to specify a root task, or > is that part of the minimal environment? You will still need to provide a root task application. sel4runtime is only responsible for handling process startup for C applications. > * Is there a specific recommended location for the sel4runtime repo? The sel4runtime repo is usually placed in the projects directory. You can see sel4-tutorials-manifest[^1] repository on github for an example of how the dependecies are laid out. [^1]: https://github.com/SEL4PROJ/sel4-tutorials-manifest Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

2 1

[FOSDEM] [Fwd: CfP: FOSDEM 2020 - Microkernels and Component-based OS devroom] (fwd)
by Stefan Kalkowski 04 Oct '19

04 Oct '19

Hello sel4 community, I think below announcement might be interesting for you too. Best regards Stefan Kalkowski -------- Forwarded Message -------- From: Julian Stecklina <js(a)alien8.de> Reply-To: microkernel-devroom(a)lists.fosdem.org To: l4-hackers(a)os.inf.tu-dresden.de, users(a)lists.genode.org, microkernel-devroom(a)lists.fosdem.org, ukvly-announce(a)freelists.org, helenos-devel(a)lists.modry.cz Subject: CfP: FOSDEM 2020 - Microkernels and Component-based OS devroom Date: Fri, 04 Oct 2019 00:38:35 +0200 [Resent due to wrong Reply-To: header] FOSDEM 2020 - Microkernels and Component-based OS devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2020 [1] in Brussels, Belgium and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-, unikernel-, and component-based operating systems. Possible topics include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * used languages and tools * enabling support for hardware (architectures, device drivers) * enabling support for programming languages * maintenance and testing * security and robustness * trends and challenges * use cases, experiences, lessons learned and demos The deadline for your proposal is on December 1, 2019. Please use the Pentabarf [2] system to submit your proposals. You do not need to create a new account if you already have one. Make sure to include the following in your proposal: * title of your talk (will be printed in the FOSDEM booklet) * your full name (will be printed in the FOSDEM booklet) * a short abstract (one or two paragraphs) * duration of your talk (at least 25 and no longer than 55 min) The official devroom schedule (along with the accepted talks) will be announced on December 15 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. You are invited to send any other suggestions for what you want to see or do at the devroom to the list. We will also use this list to organize the traditional devroom dinner that will happen on the first day of FOSDEM. About the devroom Since the first Microkernel devroom at FOSDEM 2012, this devroom has been part of each following FOSDEM. The focus gradually widened to include component-based operating systems. By now it has become a somewhat institutionalized tradition for the community to meet there; to this date over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Social events It also has become a habit that the microkernel projects dine together somewhere in Brussels. The year 2020 will not be any different, so there is going to be a dinner on Saturday night. We try place a reservation, so we will inform you about the exact location and time later. Consult the FOSDEM web and other projects for additional social events such as the famous FOSDEM-organized Friday Beer Event and the FOSDEM-arranged free sightseeing tours for spouses. About FOSDEM FOSDEM is a two-day event organised by volunteers to promote the widespread use of free and open source software. Taking place in the beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the best such conference in Europe. FOSDEM covers a wide spectrum of free and open source software projects, and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) with network/internet connectivity and projectors where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and discussions. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. Every year, FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. Participation and attendance is totally free, though the organisers gratefully accept donations and sponsorship. No registration necessary. Important dates recap * 2019-12-01: Deadline for submissions * 2019-12-15: Schedule published and speakers notified of acceptance * 2020-02-01: Devroom Dinner (details to be announced) * 2020-02-01/2020-02-02: The devroom takes places (check the schedule) Links [1] https://fosdem.org/ [2] https://penta.fosdem.org/submission/FOSDEM20 [3] https://lists.fosdem.org/listinfo/microkernel-devroom _______________________________________________ FOSDEM mailing list FOSDEM(a)lists.fosdem.org https://lists.fosdem.org/listinfo/fosdem ----- End forwarded message ----- -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

1 0

Re: [seL4] CapDL output to isabelle file
by Lim, Japheth (Data61, Kensington NSW) 03 Oct '19

03 Oct '19

Hi Norrathep, Norrathep Rattanavipanon wrote: > I have been trying to generate Isabelle file from CapDL specification. But > I run into an error when I'm running the command: > > ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml > example-arm.cdl > We recently put in a major change to the Isabelle translator. The input capDL file is now required to be pre-allocated, i.e. every object must be placed in an untyped with a known physical address. The existing example files date from before this change, and so they don't meet the requirements to be translated into Isabelle. Sorry that you got confusing error messages as a result. We plan to make this more consistent in the near future. > Is there any step I'm missing? Or does the tool not support the conversion > to Isabelle? The standard way is to build a CAmkES application with the option `CAmkESCapDLStaticAlloc` enabled. This will generate a suitable capDL file for proofs. Based on your other question thread, you may be interested in our README for CAmkES proofs: https://github.com/seL4/camkes-tool/tree/master/cdl-refine-tests This generates proofs between the CAmkES high-level model and the capDL system representation. However, we are not working on C glue code proofs at the moment. This is all work in progress, and quite rough around the edges. Nevertheless, we're happy to try to answer any questions you might have. It would help if we knew more about your work, so that we can give more specific replies. Cheers, Japheth Lim Proof Engineer, Trustworthy Systems

3 5