Re: [PATCH] c-user: Add application config info directives

2022-09-19 Thread Chris Johns 
On 19/9/2022 5:21 pm, Sebastian Huber wrote:
> On 17/09/2022 09:31, Chris Johns wrote:
>>> +rtems_configuration_get_do_zero_of_workspace()
>>> +--
>>> +
>>> +Indicates if the RTEMS Workspace is configured to be zeroed during system
>>> +initialization for this application.
>>> +
>>> +.. rubric:: CALLING SEQUENCE:
>>> +
>>> +.. code-block:: c
>>> +
>>> +    #define rtems_configuration_get_do_zero_of_workspace()
>>> +
>>> +.. rubric:: RETURN VALUES:
>>> +
>>> +Returns true, if the RTEMS Workspace is configured to be zeroed during 
>>> system
>>> +initialization for this application, otherwise false.
>> Should the type returned be specified?
> 
> Historically, these rtems_configuration_get*() directives are implemented as a
> macro. We could change them to inline functions to get a typed interface.

Or just provide the type in the doco to guide the user. For example which is the
one to use and not get warnings from a pedantic compiler:

  unsigned long long v = rtems_configuration_get_do_zero_of_workspace();
  float v = rtems_configuration_get_do_zero_of_workspace();
  bool v = rtems_configuration_get_do_zero_of_workspace();
  int v = rtems_configuration_get_do_zero_of_workspace();

?

Chris
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Successful Hello world from RPi4B AArch64 over serial

2022-09-19 Thread Joel Sherrill 
On Mon, Sep 19, 2022, 1:23 PM Alan Cudmore  wrote:

> I built the TF-A binary, your dev branch, used the config.txt described
> below, and was able to run unlimited.exe. (I’m using a Pi4b 2GB)
>
> Great milestone!
>

This is great news! Now to get it merged for others.

Are any other peripherals from previous Pi generations the same? Curious if
wired networking might be low hanging fruit.

--joel

> Alan
>
>
>
> *From: *Noor Aman 
> *Sent: *Monday, September 19, 2022 11:11 AM
> *To: *William Moore ; Alan Cudmore
> ; Hesham Moustafa ;
> rtems-de...@rtems.org 
> *Subject: *Successful Hello world from RPi4B AArch64 over serial
>
>
>
> Hey everyone,
>
> I've managed to get RTEMS6 on the Raspberry pi 4B rev 1.4. Every test ran
> fine except for minimum.exe, It gave a fatal error.
>
>
>
> Here's my setup for running RTEMS6 on RPi4B:
>
>
>
> TF-A is required to enable GIC on RPi. I had tried to use armstub-gic.S (
> https://github.com/raspberrypi/tools/blob/master/armstubs/armstub8.S) but
> it didn't work out. TF-A on other hand did work pretty well.
>
>
>
> Steps to get TF-A binary are described here:
> https://trustedfirmware-a.readthedocs.io/en/latest/plat/rpi4.html
>
>
>
> Config.txt section:
>
> arm_64bit=1
> enable_uart=1
> gpio=22-27=np
> enable_jtag_gpio=1
> dtoverlay=disable-bt
> kernel=kernel8.img
> enable_gic=1
> armstub=bl31.bin
>
>
>
> RTEMS6
>
> My branch (noov-dev): https://github.com/0xnoor/rtems/tree/noor-dev
>
>
>
>
> ___
> devel mailing list
> devel@rtems.org
> http://lists.rtems.org/mailman/listinfo/devel
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: OT: [PATCH rtems-lwip v3 1/7] lwip.py: Change arch and bsp check method

2022-09-19 Thread Kinsey Moore 

On 9/19/2022 04:28, Cedric Berger wrote:

Sorry for a slightly off-topic question here:

[...]
In that case, I'll stick with the BSP management improvements once v4 
of this patch set goes in (probably) and skip the generic build.


Is a generic build something that would be worth pursuing for lwIP? 
It would come with the core stacks, but no drivers whatsoever.


I'm very exited about that stuff, and here is a project I'm entertaining:

Using LWIP on the Cortex-M4 side of a stm32h747:

 - Without the ethernet driver.

 - With an emulated, ethernet USB driver (device-side USB, I will 
write the driver if it does not exist yet).


 - Talking to a cellular modem with PPP over USB (host-side USB, I 
will write the driver if it does not exist yet).


Can I, today, configure a basic/generic LWIP stack that would allow to 
develop such a setup?



Currently all rtems-lwip build configurations are very BSP-specific and 
include drivers with no options to leave the drivers out of the build. 
Additionally, there is no option for a generic build for BSPs that 
aren't specifically supported.


It's possible that we could build a generic stack for BSPs that aren't 
otherwise supported with drivers, but I'm waiting on some things to 
settle out (specifically STM32F4 support) before I move forward with any 
more changes that could disrupt that.


I'm also focused elsewhere for the moment, so waiting on things to 
settle out is fine.



Kinsey

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

RE: Successful Hello world from RPi4B AArch64 over serial

2022-09-19 Thread Alan Cudmore 
I built the TF-A binary, your dev branch, used the config.txt described below, and was able to run unlimited.exe. (I’m using a Pi4b 2GB)Great milestone!Alan From: Noor AmanSent: Monday, September 19, 2022 11:11 AMTo: William Moore; Alan Cudmore; Hesham Moustafa; rtems-de...@rtems.orgSubject: Successful Hello world from RPi4B AArch64 over serial Hey everyone, I've managed to get RTEMS6 on the Raspberry pi 4B rev 1.4. Every test ran fine except for minimum.exe, It gave a fatal error. Here's my setup for running RTEMS6 on RPi4B: TF-A is required to enable GIC on RPi. I had tried to use armstub-gic.S (https://github.com/raspberrypi/tools/blob/master/armstubs/armstub8.S) but it didn't work out. TF-A on other hand did work pretty well.  Steps to get TF-A binary are described here: https://trustedfirmware-a.readthedocs.io/en/latest/plat/rpi4.html Config.txt section:arm_64bit=1enable_uart=1gpio=22-27=npenable_jtag_gpio=1dtoverlay=disable-btkernel=kernel8.imgenable_gic=1armstub=bl31.bin RTEMS6 My branch (noov-dev): https://github.com/0xnoor/rtems/tree/noor-dev  
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH v2 0/4] Microchip PolarFire SoC support

2022-09-19 Thread Alan Cudmore 
Hi Padmarao,
The patches apply cleanly and build for me. What is the recommended
config.ini file for this BSP?
I used:
[riscv/mpfs64imafdc]
BUILD_TESTS=True
RTEMS_POSIX_API=True
RTEMS_SMP=True
BSP_START_COPY_FDT_FROM_U_BOOT=False
BSP_DTB_IS_SUPPORTED=True
BSP_DTB_HEADER_PATH=bsp/mpfs-dtb.h

I don't have a Polarfire SoC board, but is there a QEMU platform to run
this on?

When this is in, I will rebase my k210 variant and eventually get it
submitted!
Thanks,
Alan

On Mon, Sep 19, 2022 at 9:00 AM Padmarao Begari <
padmarao.beg...@microchip.com> wrote:

> This patch set adds the Microchip PolarFire SoC BSP Variant
> support to RISC-V RTEMS.
>
> The PolarFire SoC is the 4x 64-bit RISC-V U54 cores and
> a 64-bit RISC-V E51 monitor core SoC from Microchip, more
> info available here:
> https://www.microchip.com/en-us/products/fpgas-and-plds/
> system-on-chip-fpgas/polarfire-soc-fpgas#Overview
>
> This new BSP variant is added for the 4x U54 cores not for E51
> because the E51 monitor core is resreved for first stage
> bootloader (Hart Software Services).
>
> The boot HARTID configurable is implemented for the riscv BSP
> to work with individual hart(cpu core) or SMP.
>
> This BSP support components: 4 CPU Cores (U54), Interrupt
> controller (PLIC), Timer (CLINT), UART (16550-compatible)
> work fine on actual Microchip PolarFire SoC Icicle Kit.
>
> v2:
> - Add a license and copyright information in dtb header file
> - Use RISCV_BOOT_HARDID instead of RTEMS_BOOT_HARDID
> - Add '_RISCV_Map_hardid_to_cpu_index()' and
> '_RISCV_Map_cpu_index_to_hardid()' functions
> - Change bsp_fdt_get() instead of bsp_fdt_copy() function for dtb
> - Move dtb and dtb header configurable build option to the bsps
>
> Padmarao Begari (4):
>   bsps/riscv: Add device tree blob
>   spec/build/bsps: Add dtb support
>   bsps/riscv: Add Microchip PolarFire SoC BSP variant
>   bsps/shared/: Use device tree blob
>
>  bsps/riscv/riscv/clock/clockdrv.c |   6 +-
>  bsps/riscv/riscv/config/mpfs64imafdc.cfg  |   9 +
>  bsps/riscv/riscv/dts/mpfs.dts | 365 +++
>  bsps/riscv/riscv/include/bsp/mpfs-dtb.h   | 602 ++
>  bsps/riscv/riscv/include/bsp/riscv.h  |  14 +
>  bsps/riscv/riscv/irq/irq.c|  81 +++
>  bsps/riscv/riscv/start/bsp_fatal_halt.c   |   3 +
>  bsps/riscv/riscv/start/bspsmp.c   |   2 +-
>  bsps/riscv/riscv/start/bspstart.c |  19 +-
>  bsps/riscv/shared/start/start.S   |   2 +
>  bsps/shared/start/bsp-fdt.c   |   8 +
>  .../score/cpu/riscv/include/rtems/score/cpu.h |   2 +-
>  .../cpu/riscv/include/rtems/score/cpuimpl.h   |   2 +-
>  spec/build/bsps/optdtb.yml|  19 +
>  spec/build/bsps/optdtbheaderpath.yml  |  20 +
>  spec/build/bsps/riscv/optextirqmax.yml|   5 +-
>  spec/build/bsps/riscv/optrambegin.yml |   5 +-
>  spec/build/bsps/riscv/optramsize.yml  |   5 +-
>  spec/build/bsps/riscv/riscv/abi.yml   |   6 +
>  .../bsps/riscv/riscv/bspmpfs64imafdc.yml  |  19 +
>  spec/build/bsps/riscv/riscv/grp.yml   |   6 +
>  spec/build/bsps/riscv/riscv/optmpfs.yml   |  18 +
>  spec/build/bsps/riscv/riscv/optns16550max.yml |   3 +
>  spec/build/cpukit/cpuopts.yml |   2 +
>  spec/build/cpukit/optarchbits.yml |   1 +
>  spec/build/cpukit/optboothartid.yml   |  19 +
>  spec/build/cpukit/optsmp.yml  |   1 +
>  27 files changed, 1235 insertions(+), 9 deletions(-)
>  create mode 100644 bsps/riscv/riscv/config/mpfs64imafdc.cfg
>  create mode 100644 bsps/riscv/riscv/dts/mpfs.dts
>  create mode 100644 bsps/riscv/riscv/include/bsp/mpfs-dtb.h
>  create mode 100644 spec/build/bsps/optdtb.yml
>  create mode 100644 spec/build/bsps/optdtbheaderpath.yml
>  create mode 100644 spec/build/bsps/riscv/riscv/bspmpfs64imafdc.yml
>  create mode 100644 spec/build/bsps/riscv/riscv/optmpfs.yml
>  create mode 100644 spec/build/cpukit/optboothartid.yml
>
> --
> 2.25.1
>
> ___
> devel mailing list
> devel@rtems.org
> http://lists.rtems.org/mailman/listinfo/devel
>
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Successful Hello world from RPi4B AArch64 over serial

2022-09-19 Thread Alan Cudmore 
Great progress Noor!
I will try your branch today.
Alan

On Mon, Sep 19, 2022 at 12:15 PM Joel Sherrill  wrote:

>
>
> On Mon, Sep 19, 2022 at 10:11 AM Noor Aman  wrote:
>
>> Hey everyone,
>> I've managed to get RTEMS6 on the Raspberry pi 4B rev 1.4. Every test ran
>> fine except for minimum.exe, It gave a fatal error.
>>
>
> Congratulations! Hoozah!
>
> minimum.exe is supposed to reflect the smallest application you can have.
> It barely qualifies as an application as the Initialization task exits
> from the
> thread body and that's what triggers the fatal error. It is expected so
> that's a
> pass. Unfortunately, the exception frame you posted to Discord has what
> looks like a mistake in printing the idle thread id (see name on next
> line):
>
> *** FATAL ***
> fatal source: 0 (INTERNAL_ERROR_CORE)
> fatal code: 5 (INTERNAL_ERROR_THREAD_EXITTED)
> RTEMS version: 6.0.0.ee92899632c823e19aa4f2e7048af3d910f59be2
> RTEMS tools: 12.1.1 20220622 (RTEMS 6, RSB
> eea379370116628dbe91f19e61ad6129aa1951ac, Newlib ea99f21)
> executing thread ID: 0x089010001   <
> executing thread name: IDLE
>
>
> Kinsey can you run this on one of the aarch64 bit targets you have?
> I suspect this is not a Pi specific issue but maybe something in
> printk? Or the printf format specifier used.  Once more is known, this
> likely will need a ticket.
>
> Try the fileio, cdtest, nsecs, and paranoia samples next. If those
> look ok, it is highly likely that most of the single processor tests
> will run.
>
> fileio requires working console input.
>
>
>>
>> Here's my setup for running RTEMS6 on RPi4B:
>>
>> TF-A is required to enable GIC on RPi. I had tried to use armstub-gic.S (
>> https://github.com/raspberrypi/tools/blob/master/armstubs/armstub8.S)
>> but it didn't work out. TF-A on other hand did work pretty well.
>>
>> Steps to get TF-A binary are described here:
>> https://trustedfirmware-a.readthedocs.io/en/latest/plat/rpi4.html
>>
>
>
>>
>> Config.txt section:
>> arm_64bit=1
>> enable_uart=1
>> gpio=22-27=np
>> enable_jtag_gpio=1
>> dtoverlay=disable-bt
>> kernel=kernel8.img
>> enable_gic=1
>> armstub=bl31.bin
>>
>> RTEMS6
>> My branch (noov-dev): https://github.com/0xnoor/rtems/tree/noor-dev
>>
>
> Now work to get this all cleaned up, merged, and documented. Kinsey
> now has a Pi4 ready to double check your work is repeatable from
> rtems.org sources.
>
> --joel
>
>>
>> ___
>> devel mailing list
>> devel@rtems.org
>> http://lists.rtems.org/mailman/listinfo/devel
>
>
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Successful Hello world from RPi4B AArch64 over serial

2022-09-19 Thread Joel Sherrill 
On Mon, Sep 19, 2022 at 10:11 AM Noor Aman  wrote:

> Hey everyone,
> I've managed to get RTEMS6 on the Raspberry pi 4B rev 1.4. Every test ran
> fine except for minimum.exe, It gave a fatal error.
>

Congratulations! Hoozah!

minimum.exe is supposed to reflect the smallest application you can have.
It barely qualifies as an application as the Initialization task exits from
the
thread body and that's what triggers the fatal error. It is expected so
that's a
pass. Unfortunately, the exception frame you posted to Discord has what
looks like a mistake in printing the idle thread id (see name on next line):

*** FATAL ***
fatal source: 0 (INTERNAL_ERROR_CORE)
fatal code: 5 (INTERNAL_ERROR_THREAD_EXITTED)
RTEMS version: 6.0.0.ee92899632c823e19aa4f2e7048af3d910f59be2
RTEMS tools: 12.1.1 20220622 (RTEMS 6, RSB
eea379370116628dbe91f19e61ad6129aa1951ac, Newlib ea99f21)
executing thread ID: 0x089010001   <
executing thread name: IDLE


Kinsey can you run this on one of the aarch64 bit targets you have?
I suspect this is not a Pi specific issue but maybe something in
printk? Or the printf format specifier used.  Once more is known, this
likely will need a ticket.

Try the fileio, cdtest, nsecs, and paranoia samples next. If those
look ok, it is highly likely that most of the single processor tests
will run.

fileio requires working console input.


>
> Here's my setup for running RTEMS6 on RPi4B:
>
> TF-A is required to enable GIC on RPi. I had tried to use armstub-gic.S (
> https://github.com/raspberrypi/tools/blob/master/armstubs/armstub8.S) but
> it didn't work out. TF-A on other hand did work pretty well.
>
> Steps to get TF-A binary are described here:
> https://trustedfirmware-a.readthedocs.io/en/latest/plat/rpi4.html
>


>
> Config.txt section:
> arm_64bit=1
> enable_uart=1
> gpio=22-27=np
> enable_jtag_gpio=1
> dtoverlay=disable-bt
> kernel=kernel8.img
> enable_gic=1
> armstub=bl31.bin
>
> RTEMS6
> My branch (noov-dev): https://github.com/0xnoor/rtems/tree/noor-dev
>

Now work to get this all cleaned up, merged, and documented. Kinsey
now has a Pi4 ready to double check your work is repeatable from
rtems.org sources.

--joel

>
> ___
> devel mailing list
> devel@rtems.org
> http://lists.rtems.org/mailman/listinfo/devel
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH] bsps/riscv/riscv: Fix fe310_uart_read

2022-09-19 Thread Sebastian Huber 

On 18/09/2022 21:22, Alan Cudmore wrote:

Note: Resending after learning how to use git send-email, please disregard 
previous message.

This fixes the riscv fe310 console driver fe310_uart_read function. The function
reads the RX status/data register to check if data is available, but discards
the data and reads it a seconds time.
Also cleared the interrupt enable bit in the first_open function.

Close #4719


Thanks, I checked it in.

--
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Successful Hello world from RPi4B AArch64 over serial

2022-09-19 Thread Noor Aman 
Hey everyone,
I've managed to get RTEMS6 on the Raspberry pi 4B rev 1.4. Every test ran
fine except for minimum.exe, It gave a fatal error.

Here's my setup for running RTEMS6 on RPi4B:

TF-A is required to enable GIC on RPi. I had tried to use armstub-gic.S (
https://github.com/raspberrypi/tools/blob/master/armstubs/armstub8.S) but
it didn't work out. TF-A on other hand did work pretty well.

Steps to get TF-A binary are described here:
https://trustedfirmware-a.readthedocs.io/en/latest/plat/rpi4.html

Config.txt section:
arm_64bit=1
enable_uart=1
gpio=22-27=np
enable_jtag_gpio=1
dtoverlay=disable-bt
kernel=kernel8.img
enable_gic=1
armstub=bl31.bin

RTEMS6
My branch (noov-dev): https://github.com/0xnoor/rtems/tree/noor-dev
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Fwd: FSW-2023 Registration is now open! Secure your ticket

2022-09-19 Thread Joel Sherrill 
Hi

This is the first in-person FSW since before COVID. This is a workshop
focused on space going applications. The presentations tend to be very
interesting and top notch. Plus the opportunity to speak with others in the
field is really incredible.

OAR is planning to be there including myself and a few others. Gaisler
usually is represented as well. Hopefully others will be able to attend as
well.

--joel


 Forwarded Message 
Subject:FSW-2023 Registration is now open! Secure your ticket
Date:   Fri, 16 Sep 2022 18:00:18 -0400 (EDT)
From:   Flight Software Workshop 
Reply-To:   i...@flightsoftware.org
To: joel.sherr...@oarcorp.com



Flight software workshop: March 20 to 23, 2023 at Caltech/JPL
Dear Joel,

Registration is open for 2023 Flight Software Workshop, which will be in
person at Caltech in Pasadena, CA on March 20, 2023 to March 23, 2023.
  We hope you will join us for a week of flight software discussion and
knowledge-sharing.

Register for FSW-2023 here!
<
https://r20.rs6.net/tn.jsp?f=001F4LSfUx-u8pMPB_uq4Kb7F1RFzB29_X2YN2xRJ8EkG_QvTOowjCo2Y5o6-0297qZi7_e62PU0flSackTTxx5M5LmS7IBU0XZ_If75HdFHNRmRqpl2I5PHW8beRhQvAQiw-iwrRrr6G21snEcnqqwpyAZcxLdLwEWJIYdGc2Gi-W3JffDA2piuttuszN2Ldr8IGtOqccd3ygMXHzV2UHyZNlz-GtgOmvL=vpTyfEz6YELgKOJNCWjyCj022AxYPw-idGcVy6HxH4IRtDoLgeG7fg===Mi3ZzLFyaismnwMWolLZUSl8J6cBnok1rcYjls8ODvl_3hnoeeYMew==>



Sign up for our mailing list
<
https://r20.rs6.net/tn.jsp?f=001F4LSfUx-u8pMPB_uq4Kb7F1RFzB29_X2YN2xRJ8EkG_QvTOowjCo2Y5o6-0297qZtYIJcq6enlPpg3TZ9KNRzOE77ZKdINNFjUgfrkErFcF-8ONefy83s51_u0clCDtxzKdrphq9_ItuRuX9-N4xKygsJg6Fkg133TPe1CrGpfqN4oxw5AvXObtLsPUPrZdvwl0CgY3OxBpgwfkeVsaitDh4dto5JsvYmZ2LDOfZfNamHWFoonJOw_SfIiocMjYUz0Z4Bjz4II-y9Dlb7keMpYnvceeFmE5PZOSkJcWhmMyrDwScAgRXe5cQ1p4gBW_-C-TMRzyOKVeqV5IFnVUhNw===vpTyfEz6YELgKOJNCWjyCj022AxYPw-idGcVy6HxH4IRtDoLgeG7fg===Mi3ZzLFyaismnwMWolLZUSl8J6cBnok1rcYjls8ODvl_3hnoeeYMew==>
to

keep up to date on FSW-2023.

FSW-2023 Workshop Cycle



Registration Opens: September 16, 2022-- TODAY!

First Call for Abstracts: October 1, 2022

Abstract Submission Deadline: December 12, 2022

Abstract Acceptance Notification: January 15, 2023

Presentation Submission Deadline: February 20, 2023

Workshop: March 20-23, 2023

The Flight Software Workshop is continuing its 16-year tradition of
emphasizing the latest technical content in an informal setting. The
workshop provides an opportunity to present current flight software
architectures, novel approaches to mission solutions, and techniques for
flight software development, integration, test, and verification.

FSW-2023 Topics

General themes for Flight Software Workshop:

   * Artificial intelligence, machine learning, and onboard data processing
   * Space networking
   * Onboard data storage and representation
   * Flight software architectures, frameworks, and software buses
   * Software enabled mission concepts
   * Digital twin, config management, and software enabled emulation
   * DevOps, continuous integration, and automated testing
   * FSW, embedded processor, and FPGA interactions
   * Flight Operating Systems
   * New languages (bring your non-C work)
   * Your hot FSW topic we haven't listed!

Please note: Themes are suggested topics, meant to guide and inspire
Workshop participants. Other flight software subjects are welcome for
consideration!



Demos and Workshop Sessions

We would like to encourage the community to get hands-onat FSW Workshop
2023! While we will continue our presentation tracks, we recommend
considering submitting your hardware and software demonstration, as well
as your workshop ideas.


Check your inbox on October 1(FSW-2023 Call for Abstracts) for
instructions on how to submit your abstract for a presentation, demo, or
workshop this year!





The Aerospace Corporation, NASA Jet Propulsion Laboratory, Southwest
Research Institute, and The Johns Hopkins University Applied Physics
Laboratory are the Founding Sponsors of the Flight Software Workshop.
Additional sponsorship opportunities exist for the 2023 Workshop. Please
email inquiries to Violet Torossian (Sponsor Relations) at
spon...@flightsoftware.org .

More information about this year's Workshop can be found at the 2023
Workshop Home Page
<
https://r20.rs6.net/tn.jsp?f=001F4LSfUx-u8pMPB_uq4Kb7F1RFzB29_X2YN2xRJ8EkG_QvTOowjCo2Q81GblSU-4ACmU_PwP-JpXrT6JZoNa6dVwA9YbqcSd0RHnJLELIBtsjHWiY8bH0sJnjTia4Gdpwc6RFIp1UUlWDrx3EGf8Tzg===vpTyfEz6YELgKOJNCWjyCj022AxYPw-idGcVy6HxH4IRtDoLgeG7fg===Mi3ZzLFyaismnwMWolLZUSl8J6cBnok1rcYjls8ODvl_3hnoeeYMew==>.

All prior years' recorded and pre-recorded presentations can be found on
our FSW Workshop YouTube playlist page
<

[PATCH v2 2/4] spec/build/bsps: Add dtb support

2022-09-19 Thread Padmarao Begari 
Add dtb and dtb header path configurable build option
---
 spec/build/bsps/optdtb.yml   | 19 +++
 spec/build/bsps/optdtbheaderpath.yml | 20 
 2 files changed, 39 insertions(+)
 create mode 100644 spec/build/bsps/optdtb.yml
 create mode 100644 spec/build/bsps/optdtbheaderpath.yml

diff --git a/spec/build/bsps/optdtb.yml b/spec/build/bsps/optdtb.yml
new file mode 100644
index 00..54ae7aa770
--- /dev/null
+++ b/spec/build/bsps/optdtb.yml
@@ -0,0 +1,19 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+actions:
+- get-boolean: null
+- define-condition: null
+build-type: option
+copyrights:
+- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+default: false
+default-by-variant:
+- value: true
+  variants:
+  - riscv/mpfs64.*
+description: |
+  the path to the header file containing the device tree binary. See the BSP
+  documentation for more information.
+enabled-by: true
+links: []
+name: BSP_DTB_IS_SUPPORTED
+type: build
diff --git a/spec/build/bsps/optdtbheaderpath.yml 
b/spec/build/bsps/optdtbheaderpath.yml
new file mode 100644
index 00..7e294ce058
--- /dev/null
+++ b/spec/build/bsps/optdtbheaderpath.yml
@@ -0,0 +1,20 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+actions:
+- get-string: null
+- define: null
+build-type: option
+copyrights:
+- Copyright (C) 2022 On-Line Applications Research Corporation (OAR)
+default: false
+default-by-variant:
+- value: bsp/mpfs-dtb.h
+  variants:
+  - riscv/mpfs64.*
+description: |
+  the path to the header file containing the device tree binary. See the BSP
+  documentation for more information.
+enabled-by: true
+format: '{}'
+links: []
+name: BSP_DTB_HEADER_PATH
+type: build
-- 
2.25.1

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

[PATCH v2 1/4] bsps/riscv: Add device tree blob

2022-09-19 Thread Padmarao Begari 
Add the basic Microchip PolarFire SoC device tree source and blob

The mpfs-dtb.h is generated by the bin2hex

https://github.com/padmaraob/bin2hex

1.Compile and build the bin2hex.c
$ gcc -o bin2hex bin2hex.c

2.Generate the mpfs.dtb from the mpfs.dts
$ dtc -O dtb -o mpfs.dtb mpfs.dts

3.Generate the mpfs-dtb.h Header file from the mpfs.dtb.
$ ./bin2hex mpfs.dtb
---
 bsps/riscv/riscv/dts/mpfs.dts   | 365 ++
 bsps/riscv/riscv/include/bsp/mpfs-dtb.h | 602 
 2 files changed, 967 insertions(+)
 create mode 100644 bsps/riscv/riscv/dts/mpfs.dts
 create mode 100644 bsps/riscv/riscv/include/bsp/mpfs-dtb.h

diff --git a/bsps/riscv/riscv/dts/mpfs.dts b/bsps/riscv/riscv/dts/mpfs.dts
new file mode 100644
index 00..7b19701b02
--- /dev/null
+++ b/bsps/riscv/riscv/dts/mpfs.dts
@@ -0,0 +1,365 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/*
+ * Copyright (C) Padmarao Begari 
+ * Copyright (C) 2022 Microchip Technology Inc.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/dts-v1/;
+
+/ {
+   #address-cells = <2>;
+   #size-cells = <2>;
+
+   model = "Microchip PolarFire-SoC Icicle Kit";
+   compatible = "microchip,mpfs-icicle-kit", "microchip,mpfs";
+
+   aliases {
+   serial1 = 
+   ethernet0 = 
+   };
+
+   chosen {
+   stdout-path = "serial1";
+   };
+
+   cpucomplex: cpus {
+   #address-cells = <1>;
+   #size-cells = <0>;
+
+   timebase-frequency = <100>;
+
+   cpu0: cpu@0 {
+   clock-frequency = <0>;
+   compatible = "sifive,e51", "sifive,rocket0", "riscv";
+   device_type = "cpu";
+   i-cache-block-size = <64>;
+   i-cache-sets = <128>;
+   i-cache-size = <16384>;
+   reg = <0>;
+   riscv,isa = "rv64imac";
+   status = "disabled";
+   cpu0intc: interrupt-controller {
+   #interrupt-cells = <1>;
+   compatible = "riscv,cpu-intc";
+   interrupt-controller;
+   };
+   };
+   cpu1: cpu@1 {
+   clock-frequency = <0>;
+   compatible = "sifive,u54-mc", "sifive,rocket0", "riscv";
+   d-cache-block-size = <64>;
+   d-cache-sets = <64>;
+   d-cache-size = <32768>;
+   d-tlb-sets = <1>;
+   d-tlb-size = <32>;
+   device_type = "cpu";
+   i-cache-block-size = <64>;
+   i-cache-sets = <64>;
+   i-cache-size = <32768>;
+   i-tlb-sets = <1>;
+   i-tlb-size = <32>;
+   mmu-type = "riscv,sv39";
+   reg = <1>;
+   riscv,isa = "rv64imafdc";
+   tlb-split;
+   status = "okay";
+   cpu1intc: interrupt-controller {
+   #interrupt-cells = <1>;
+   compatible = "riscv,cpu-intc";
+   interrupt-controller;
+   };
+   };
+
+   cpu2: cpu@2 {
+   clock-frequency = <0>;
+   compatible = "sifive,u54-mc", "sifive,rocket0", "riscv";
+   d-cache-block-size = <64>;
+   d-cache-sets =

[PATCH v2 4/4] bsps/shared/: Use device tree blob

2022-09-19 Thread Padmarao Begari 
If the bsp is integrated and supported a device tree
blob(dtb) then use dtb instead of using it from
the U-Boot (BSP_START_COPY_FDT_FROM_U_BOOT=False).
---
 bsps/shared/start/bsp-fdt.c | 8 
 1 file changed, 8 insertions(+)

diff --git a/bsps/shared/start/bsp-fdt.c b/bsps/shared/start/bsp-fdt.c
index 75a1ea41c9..f532247b2a 100644
--- a/bsps/shared/start/bsp-fdt.c
+++ b/bsps/shared/start/bsp-fdt.c
@@ -32,6 +32,10 @@
 #include 
 #include 
 
+#ifdef BSP_DTB_IS_SUPPORTED
+#include BSP_DTB_HEADER_PATH
+#endif
+
 #ifndef BSP_FDT_IS_SUPPORTED
 #warning "BSP FDT support indication not defined"
 #endif
@@ -76,5 +80,9 @@ void bsp_fdt_copy(const void *src)
 
 const void *bsp_fdt_get(void)
 {
+#ifdef BSP_DTB_IS_SUPPORTED
+  return system_dtb;
+#else
   return _fdt_blob[0];
+#endif
 }
-- 
2.25.1

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

[PATCH v2 3/4] bsps/riscv: Add Microchip PolarFire SoC BSP variant

2022-09-19 Thread Padmarao Begari 
The Microchip PolarFire SoC support is implemented as a
riscv BSP variant to boot with any individual hart(cpu core)
or SMP based on the boot HARTID configurable and support
components are 4 CPU Cores (U54), Interrupt controller (PLIC),
Timer (CLINT), UART.
---
 bsps/riscv/riscv/clock/clockdrv.c |  6 +-
 bsps/riscv/riscv/config/mpfs64imafdc.cfg  |  9 +++
 bsps/riscv/riscv/include/bsp/riscv.h  | 14 
 bsps/riscv/riscv/irq/irq.c| 81 +++
 bsps/riscv/riscv/start/bsp_fatal_halt.c   |  3 +
 bsps/riscv/riscv/start/bspsmp.c   |  2 +-
 bsps/riscv/riscv/start/bspstart.c | 19 -
 bsps/riscv/shared/start/start.S   |  2 +
 .../score/cpu/riscv/include/rtems/score/cpu.h |  2 +-
 .../cpu/riscv/include/rtems/score/cpuimpl.h   |  2 +-
 spec/build/bsps/riscv/optextirqmax.yml|  5 +-
 spec/build/bsps/riscv/optrambegin.yml |  5 +-
 spec/build/bsps/riscv/optramsize.yml  |  5 +-
 spec/build/bsps/riscv/riscv/abi.yml   |  6 ++
 .../bsps/riscv/riscv/bspmpfs64imafdc.yml  | 19 +
 spec/build/bsps/riscv/riscv/grp.yml   |  6 ++
 spec/build/bsps/riscv/riscv/optmpfs.yml   | 18 +
 spec/build/bsps/riscv/riscv/optns16550max.yml |  3 +
 spec/build/cpukit/cpuopts.yml |  2 +
 spec/build/cpukit/optarchbits.yml |  1 +
 spec/build/cpukit/optboothartid.yml   | 19 +
 spec/build/cpukit/optsmp.yml  |  1 +
 22 files changed, 221 insertions(+), 9 deletions(-)
 create mode 100644 bsps/riscv/riscv/config/mpfs64imafdc.cfg
 create mode 100644 spec/build/bsps/riscv/riscv/bspmpfs64imafdc.yml
 create mode 100644 spec/build/bsps/riscv/riscv/optmpfs.yml
 create mode 100644 spec/build/cpukit/optboothartid.yml

diff --git a/bsps/riscv/riscv/clock/clockdrv.c 
b/bsps/riscv/riscv/clock/clockdrv.c
index 65bc7c80ef..d183e65b94 100644
--- a/bsps/riscv/riscv/clock/clockdrv.c
+++ b/bsps/riscv/riscv/clock/clockdrv.c
@@ -95,6 +95,8 @@ static void riscv_clock_at_tick(riscv_timecounter *tc)
   uint64_t value;
   uint32_t cpu = rtems_scheduler_get_processor();
 
+  cpu = _RISCV_Map_cpu_index_to_hardid(cpu);
+
   clint = tc->clint;
 
   value = clint->mtimecmp[cpu].val_64;
@@ -172,6 +174,8 @@ static void riscv_clock_secondary_action(void *arg)
   uint64_t *cmpval = arg;
   uint32_t cpu = _CPU_SMP_Get_current_processor();
 
+  cpu = _RISCV_Map_cpu_index_to_hardid(cpu);
+
   riscv_clock_clint_init(clint, *cmpval, cpu);
 }
 #endif
@@ -214,7 +218,7 @@ static void riscv_clock_initialize(void)
   cmpval = riscv_clock_read_mtime(>mtime);
   cmpval += interval;
 
-  riscv_clock_clint_init(clint, cmpval, 0);
+  riscv_clock_clint_init(clint, cmpval, RISCV_BOOT_HARTID);
   riscv_clock_secondary_initialization(clint, cmpval, interval);
 
   /* Initialize timecounter */
diff --git a/bsps/riscv/riscv/config/mpfs64imafdc.cfg 
b/bsps/riscv/riscv/config/mpfs64imafdc.cfg
new file mode 100644
index 00..b04e78b0e9
--- /dev/null
+++ b/bsps/riscv/riscv/config/mpfs64imafdc.cfg
@@ -0,0 +1,9 @@
+include $(RTEMS_ROOT)/make/custom/default.cfg
+
+RTEMS_CPU = riscv
+
+CPU_CFLAGS = -march=rv64imafdc -mabi=lp64d -mcmodel=medany
+
+LDFLAGS = -Wl,--gc-sections
+
+CFLAGS_OPTIMIZE_V ?= -O2 -g -ffunction-sections -fdata-sections
diff --git a/bsps/riscv/riscv/include/bsp/riscv.h 
b/bsps/riscv/riscv/include/bsp/riscv.h
index a469155865..2ef2f8d83d 100644
--- a/bsps/riscv/riscv/include/bsp/riscv.h
+++ b/bsps/riscv/riscv/include/bsp/riscv.h
@@ -34,17 +34,31 @@
 extern "C" {
 #endif
 
+static inline uint32_t _RISCV_Map_hardid_to_cpu_index(uint32_t hardid)
+{
+  return (hardid - RISCV_BOOT_HARTID);
+}
+
+static inline uint32_t _RISCV_Map_cpu_index_to_hardid(uint32_t cpu_index)
+{
+  return (cpu_index + RISCV_BOOT_HARTID);
+}
+
 extern volatile RISCV_CLINT_regs *riscv_clint;
 
 void *riscv_fdt_get_address(const void *fdt, int node);
 
 uint32_t riscv_get_core_frequency(void);
 
+#if RISCV_ENABLE_MPFS_SUPPORT != 0
+extern uint32_t riscv_hart_count;
+#else
 #ifdef RTEMS_SMP
 extern uint32_t riscv_hart_count;
 #else
 #define riscv_hart_count 1
 #endif
+#endif
 
 uint32_t riscv_get_hart_index_by_phandle(uint32_t phandle);
 
diff --git a/bsps/riscv/riscv/irq/irq.c b/bsps/riscv/riscv/irq/irq.c
index 1b632289a6..1f383ebb89 100644
--- a/bsps/riscv/riscv/irq/irq.c
+++ b/bsps/riscv/riscv/irq/irq.c
@@ -136,6 +136,12 @@ static void riscv_clint_init(const void *fdt)
 Per_CPU_Control *cpu;
 
 hart_index = riscv_get_hart_index_by_phandle(fdt32_to_cpu(val[i / 4]));
+#ifdef RTEMS_SMP
+if (hart_index < RISCV_BOOT_HARTID) {
+  continue;
+}
+
+hart_index = _RISCV_Map_hardid_to_cpu_index(hart_index);
 if (hart_index >= rtems_configuration_get_maximum_processors()) {
   continue;
 }
@@ -143,6 +149,15 @@ static void riscv_clint_init(const void *fdt)
 cpu = _Per_CPU_Get_by_index(hart_index);
 cpu->cpu_per_cpu.clint_msip = >msip[i / 16];
 cpu->cpu_per_cpu.clint_mtimecmp =

[PATCH v2 0/4] Microchip PolarFire SoC support

2022-09-19 Thread Padmarao Begari 
This patch set adds the Microchip PolarFire SoC BSP Variant
support to RISC-V RTEMS.

The PolarFire SoC is the 4x 64-bit RISC-V U54 cores and
a 64-bit RISC-V E51 monitor core SoC from Microchip, more
info available here:
https://www.microchip.com/en-us/products/fpgas-and-plds/
system-on-chip-fpgas/polarfire-soc-fpgas#Overview

This new BSP variant is added for the 4x U54 cores not for E51
because the E51 monitor core is resreved for first stage
bootloader (Hart Software Services).

The boot HARTID configurable is implemented for the riscv BSP
to work with individual hart(cpu core) or SMP.

This BSP support components: 4 CPU Cores (U54), Interrupt
controller (PLIC), Timer (CLINT), UART (16550-compatible)
work fine on actual Microchip PolarFire SoC Icicle Kit.

v2:
- Add a license and copyright information in dtb header file
- Use RISCV_BOOT_HARDID instead of RTEMS_BOOT_HARDID
- Add '_RISCV_Map_hardid_to_cpu_index()' and
'_RISCV_Map_cpu_index_to_hardid()' functions
- Change bsp_fdt_get() instead of bsp_fdt_copy() function for dtb
- Move dtb and dtb header configurable build option to the bsps

Padmarao Begari (4):
  bsps/riscv: Add device tree blob
  spec/build/bsps: Add dtb support
  bsps/riscv: Add Microchip PolarFire SoC BSP variant
  bsps/shared/: Use device tree blob

 bsps/riscv/riscv/clock/clockdrv.c |   6 +-
 bsps/riscv/riscv/config/mpfs64imafdc.cfg  |   9 +
 bsps/riscv/riscv/dts/mpfs.dts | 365 +++
 bsps/riscv/riscv/include/bsp/mpfs-dtb.h   | 602 ++
 bsps/riscv/riscv/include/bsp/riscv.h  |  14 +
 bsps/riscv/riscv/irq/irq.c|  81 +++
 bsps/riscv/riscv/start/bsp_fatal_halt.c   |   3 +
 bsps/riscv/riscv/start/bspsmp.c   |   2 +-
 bsps/riscv/riscv/start/bspstart.c |  19 +-
 bsps/riscv/shared/start/start.S   |   2 +
 bsps/shared/start/bsp-fdt.c   |   8 +
 .../score/cpu/riscv/include/rtems/score/cpu.h |   2 +-
 .../cpu/riscv/include/rtems/score/cpuimpl.h   |   2 +-
 spec/build/bsps/optdtb.yml|  19 +
 spec/build/bsps/optdtbheaderpath.yml  |  20 +
 spec/build/bsps/riscv/optextirqmax.yml|   5 +-
 spec/build/bsps/riscv/optrambegin.yml |   5 +-
 spec/build/bsps/riscv/optramsize.yml  |   5 +-
 spec/build/bsps/riscv/riscv/abi.yml   |   6 +
 .../bsps/riscv/riscv/bspmpfs64imafdc.yml  |  19 +
 spec/build/bsps/riscv/riscv/grp.yml   |   6 +
 spec/build/bsps/riscv/riscv/optmpfs.yml   |  18 +
 spec/build/bsps/riscv/riscv/optns16550max.yml |   3 +
 spec/build/cpukit/cpuopts.yml |   2 +
 spec/build/cpukit/optarchbits.yml |   1 +
 spec/build/cpukit/optboothartid.yml   |  19 +
 spec/build/cpukit/optsmp.yml  |   1 +
 27 files changed, 1235 insertions(+), 9 deletions(-)
 create mode 100644 bsps/riscv/riscv/config/mpfs64imafdc.cfg
 create mode 100644 bsps/riscv/riscv/dts/mpfs.dts
 create mode 100644 bsps/riscv/riscv/include/bsp/mpfs-dtb.h
 create mode 100644 spec/build/bsps/optdtb.yml
 create mode 100644 spec/build/bsps/optdtbheaderpath.yml
 create mode 100644 spec/build/bsps/riscv/riscv/bspmpfs64imafdc.yml
 create mode 100644 spec/build/bsps/riscv/riscv/optmpfs.yml
 create mode 100644 spec/build/cpukit/optboothartid.yml

-- 
2.25.1

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

[PATCH] bsp/tms570: Add -mbe32 to LINKFLAGS

2022-09-19 Thread Sebastian Huber 
There is not just big-endian on ARM.  We have two variants BE32
(obsolete) and BE8.  The Cortex-R5F processor supports only BE8,
however, some TMS570 variants are BE32 internally.  In GCC 8 and later,
the --be8 option is passed to the linker based on the selected
architecture or CPU.  Use BE32 by default for the TMS570 BSP.
---
 spec/build/bsps/arm/tms570/grp.yml  |  2 ++
 spec/build/bsps/arm/tms570/optlinkflags.yml | 17 +
 2 files changed, 19 insertions(+)
 create mode 100644 spec/build/bsps/arm/tms570/optlinkflags.yml

diff --git a/spec/build/bsps/arm/tms570/grp.yml 
b/spec/build/bsps/arm/tms570/grp.yml
index 862136f7f0..60d82270c0 100644
--- a/spec/build/bsps/arm/tms570/grp.yml
+++ b/spec/build/bsps/arm/tms570/grp.yml
@@ -38,6 +38,8 @@ links:
   uid: optscibaud
 - role: build-dependency
   uid: opttms570ls3137
+- role: build-dependency
+  uid: optlinkflags
 - role: build-dependency
   uid: ../../linkcmds
 - role: build-dependency
diff --git a/spec/build/bsps/arm/tms570/optlinkflags.yml 
b/spec/build/bsps/arm/tms570/optlinkflags.yml
new file mode 100644
index 00..bf700031b7
--- /dev/null
+++ b/spec/build/bsps/arm/tms570/optlinkflags.yml
@@ -0,0 +1,17 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+actions:
+- get-string: null
+- split: null
+- env-append: LINKFLAGS
+build-type: option
+copyrights:
+- Copyright (C) 2022 embedded brains GmbH (http://www.embedded-brains.de)
+default:
+- -mbe32
+default-by-variant: []
+description: |
+  TMS570-specific flags passed to the linker.
+enabled-by: true
+links: []
+name: TMS570_LINKFLAGS
+type: build
-- 
2.35.3

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

OT: [PATCH rtems-lwip v3 1/7] lwip.py: Change arch and bsp check method

2022-09-19 Thread Cedric Berger 

Sorry for a slightly off-topic question here:

[...]
In that case, I'll stick with the BSP management improvements once v4 
of this patch set goes in (probably) and skip the generic build.


Is a generic build something that would be worth pursuing for lwIP? It 
would come with the core stacks, but no drivers whatsoever.


I'm very exited about that stuff, and here is a project I'm entertaining:

Using LWIP on the Cortex-M4 side of a stm32h747:

 - Without the ethernet driver.

 - With an emulated, ethernet USB driver (device-side USB, I will write 
the driver if it does not exist yet).


 - Talking to a cellular modem with PPP over USB (host-side USB, I will 
write the driver if it does not exist yet).


Can I, today, configure a basic/generic LWIP stack that would allow to 
develop such a setup?


Thanks for your work,

Cedric


___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Integrating the Formal Methods part of Qualification

2022-09-19 Thread andrew.butterfi...@scss.tcd.ie 
Dear Andrew,

> It's great to see a move toward formal verification for RTEMS.

Great to hear about other work in this space as well !

> From our side (TU Dortmund in Germany and the University of Twente in the 
> Netherlands), we recently adopted Frama-C to verify ICPP and MrsP. A 
> potential deadlock is successfully identified, and a remedy is provided. The 
> result will be presented in EMSOFT this year 
> (https://ieeexplore.ieee.org/document/9852753/), and the verification 
> framework is publicly released here: 
> https://github.com/tu-dortmund-ls12-rt/Resource-Synchronization-Protocols-Verification-RTEMS

Thanks for posting this - I have already  looked at and your paper pre-print - 
I like it a lot.

It complements our work very well - for example, one of the current pieces of 
our on-going work is looking at thread queues. You assume they
are implemented correctly, while we are exploring the use of model-based 
techniques to corroborate this.


> Due to the double-blind review process, I cannot chime in earlier in this 
> thread. Today earlier I have seen your patches regarding the chapter you 
> proposed. I wonder if you could take our contribution into account when you 
> organize the chapter? 
A preprint can be found 
https://www.researchgate.net/publication/362599165_Formal_Verification_of_Resource_Synchronization_Protocol_Implementations_A_Case_Study_in_RTEMS.
 (The corresponding ticket will be prepared, and the patch together with a test 
case will be submitted)

I modelled the draft formal verification chapter on the immediately preceding 
one on the Software Testing Framework.
Like it, it currently lacks much of a background/literature survey - I am 
awaiting feedback on it.
In any case, your work will be added in to anything I write about this area.

Best Regards,
  Andrew


Best,
Kuan-Hsun

On Fri, Jul 22, 2022 at 12:37 PM 
mailto:andrew.butterfi...@scss.tcd.ie 
wrote:
Dear RTEMS developers,
 
thanks for the feedback below - I want to wrap this up and move to the next 
step.
 
I propose to produce a complete draft of a formal methods section for the 
Software Engineering manual in rtems-docs
This will add a "Formal Verification" section just after the existing "Test 
Framework" section.
 
This will allow developers to get a much better idea of what is proposed, and 
for me to get feedback.
 
For now, the section will state clearly at the start that this is a proposal 
and that the tooling and resources it describes
won't yet be available in RTEMS proper. 
 
Files likely to be modified in rtems-docs:
eng/index.rst
common/refs.bib
 
I'll add in  eng/formal-verification.rst
 
I'll then submit patches for review in the usual way.
 
Regards,
  Andrew
 
 

Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/

 
 
On 11/07/2022, 12:43, "devel on behalf of 
mailto:andrew.butterfi...@scss.tcd.ie;  wrote:
 
On 6 Jul 2022, at 20:07, Gedare Bloom  wrote:
 
On Sun, Jul 3, 2022 at 7:49 PM Chris Johns  wrote:

On 2/7/2022 12:59 am, Andrew Butterfield wrote:
On 1 Jul 2022, at 00:59, Chris Johns > wrote:

On 28/6/2022 11:09 pm, mailto:andrew.butterfi...@scss.tcd.ie
 wrote:
Dear RTEMS Developers,

While the validation tests from the RTEMS pre-qualification activity are
now merged into the RTEMS master, the work done in investigating and
deploying formal methods techniques is not yet merged.

The activity had two main phases: a planning phase (Nov 2018-Oct 2019)
that explored various formal techniques, followed by an execution phase
(Oct 2019-Nov 2021) that then applied selected techniques to selected
parts of RTEMS. Some discussions occurred with the RTEMS community
via the mailings lists over this time. A short third phase (Nov 2021 - Dec 2021)
then reported on the outcomes. Each phase resulted in a technical report.

The key decision made was to use Promela/SPIN for test generation, and
to apply it to the Chains API, the Event Manager, and the SMP scheduler
thread queues. This involved developing models in the Promela language
and using the SPIN model-checker tool to both check their correctness
and to generate execution scenarios that could be used to generate tests.
Tools were developed using Python 3.8 to support this. Initial documentation
about tools and how to use them was put into the 2nd phase report.

Congratulations for the

Re: [PATCH] c-user: Add application config info directives

2022-09-19 Thread Sebastian Huber 

On 17/09/2022 09:31, Chris Johns wrote:

+rtems_configuration_get_do_zero_of_workspace()
+--
+
+Indicates if the RTEMS Workspace is configured to be zeroed during system
+initialization for this application.
+
+.. rubric:: CALLING SEQUENCE:
+
+.. code-block:: c
+
+#define rtems_configuration_get_do_zero_of_workspace()
+
+.. rubric:: RETURN VALUES:
+
+Returns true, if the RTEMS Workspace is configured to be zeroed during system
+initialization for this application, otherwise false.

Should the type returned be specified?


Historically, these rtems_configuration_get*() directives are 
implemented as a macro. We could change them to inline functions to get 
a typed interface.


--
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel