Embedded driver and funcions for bit manipulation.

[Fujii Ken-ichi]

I am building embedded drivers for RX110 series.
It is still on the way, but since the bit manipulation functions for that has been completed, it will be released.

https://github.com/fujiik102/ats-rx-drivers

Bit.sats in the above describes bit manipulation functions and the definitions necessary for them.
Bit.dats and BitInt.hats describe the implementation of the implementations and propositions of the functions (BitInt.hats is included from Bit.dats).

Pin.sats and Pin.dats are defining and implementing general-purpose I / O drivers for pins, but they are still in the middle.

Use it as you like.

[Kiwamu Okabe]

Hi Fujii,

On Sat, Aug 19, 2017 at 2:32 PM, Fujii Ken-ichi <fuji...@gmail.com> wrote:
> I am building embedded drivers for RX110 series.
> It is still on the way, but since the bit manipulation functions for that has been completed, it will be released.
>
> https://github.com/fujiik102/ats-rx-drivers

It's great work for me!

> Bit.sats in the above describes bit manipulation functions and the definitions necessary for them.
> Bit.dats and BitInt.hats describe the implementation of the implementations and propositions of the functions (BitInt.hats is included from Bit.dats).
>
> Pin.sats and Pin.dats are defining and implementing general-purpose I / O drivers for pins, but they are still in the middle.

Over future of your library, what invariant on hardware register can we capture?
For example:

* Enforce that code doesn't read and use uncertain bit
* Enforce that code doesn't start DMA without setup of buffer

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

Thanks for sharing!

I suggest the following article:

ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop

You may want to try the 'implicit' theorem-proving style and also use Z3 as
your external constraint-solver. Doing so should cut down the need for writing
a lot of theorem-proving code.

[Kiwamu Okabe]

Hi all,

On Sun, Aug 20, 2017 at 1:49 AM, gmhwxi <gmh...@gmail.com> wrote:
> You may want to try the 'implicit' theorem-proving style and also use Z3 as
> your external constraint-solver. Doing so should cut down the need for
> writing
> a lot of theorem-proving code.

I write a slide to explain the constraint-solver.

https://www.slideshare.net/master_q/ats2-updates-2017/5

[Fujii Ken-ichi]

I knew it, but I was not motivated to introduce.
Proof was hard work so, is it caused?

Thanks for the advice.
I will try it from the next.

[Fujii Ken-ichi]

Hi Okabe.

2017年8月19日土曜日 15時03分17秒 UTC+9 Kiwamu Okabe:

> Hi Fujii,
>
> On Sat, Aug 19, 2017 at 2:32 PM, Fujii Ken-ichi <fuji...@gmail.com> wrote:
> > I am building embedded drivers for RX110 series.
> > It is still on the way, but since the bit manipulation functions for that has been completed, it will be released.
> >
> > https://github.com/fujiik102/ats-rx-drivers
>
> It's great work for me!

Thanks!

>
> > Bit.sats in the above describes bit manipulation functions and the definitions necessary for them.
> > Bit.dats and BitInt.hats describe the implementation of the implementations and propositions of the functions (BitInt.hats is included from Bit.dats).
> >
> > Pin.sats and Pin.dats are defining and implementing general-purpose I / O drivers for pins, but they are still in the middle.
>
> Over future of your library, what invariant on hardware register can we capture?
> For example:
>
> * Enforce that code doesn't read and use uncertain bit

If you are saying things like a register that can read an uncertain value unless some setting is made.
So, I think there are two choices.

1.Restrict reading of registers.

Add arguments of the configuration view to the register read function.

2.Restrict　the use of reading results.

Add a snapshot of the setting view at the time of reading to the register view.

Either way, I think that we should respond individually.

> * Enforce that code doesn't start DMA without setup of buffer

I think DMA will be a problem in programming with theorem-proving.
Simplest solution is to prohibit DMA. Then we can put troubles in the trash box with usefulness.

Even if you take other methods, DMA should not be applicable to all addresses.
For example, it limits the read address of DMA to the receive register of the serial driver. In that case, the serial driver must also be designed to support DMA.

Or perhaps it is better to give up on implementation at the driver level for DMA and provide only abstract interface.

My recommendation is the first one.


In addition, List one of the other problems.

* Time measurement and impatient interrupt

When performing timing dependent processing, it is important to accurately know the current time.
But ”time” has a nasty nature that will change as we measure.
Also, we tend to think that execution time is predictable, but that is a big mistake.
For example, A fickle compiler may put in a gap of our program one million nop instructions.
Or more likely, long time interrupt handling may be inserted immediately after acquiring the current time, and the "current time" of that interrupt may be ruined.
Temporary interrupt disabled will solve the problem of interrupts, but that's the entrance to another difficulty.

One of the common requirements for embedded development is that the system is required to do something process within x micro seconds after an interrupt trigger occurs.
However, interrupt handling is not always called immediately after a trigger occurs, for example during other interrupt processing or when the interrupt is disabled.
In that case, it is necessary to limit the interrupt invalidation period and the time taken for interrupt processing.
As a solution, make an in-language language to run assembly language inline, but it is bothersome, I do not want to do it.

It is a future task.
Please tell me if you have anything amazing solution.


Best regards,

[Kiwamu Okabe]

Hi Fujii,

On Thu, Aug 31, 2017 at 1:58 PM, Fujii Ken-ichi <fuji...@gmail.com> wrote:
> If you are saying things like a register that can read an uncertain value unless some setting is made.
> So, I think there are two choices.
>
> 1.Restrict reading of registers.
>
> Add arguments of the configuration view to the register read function.
>
> 2.Restrict　the use of reading results.
>
> Add a snapshot of the setting view at the time of reading to the register view.
>
> Either way, I think that we should respond individually.

If we have HDL codes under the hardware registers, can we capture the
invariant as ATS proofs?

>> * Enforce that code doesn't start DMA without setup of buffer
>
> I think DMA will be a problem in programming with theorem-proving.
> Simplest solution is to prohibit DMA. Then we can put troubles in the trash box with usefulness.
>
> Even if you take other methods, DMA should not be applicable to all addresses.
> For example, it limits the read address of DMA to the receive register of the serial driver. In that case, the serial driver must also be designed to support DMA.
>
> Or perhaps it is better to give up on implementation at the driver level for DMA and provide only abstract interface.
>
> My recommendation is the first one.

I heard seL4 also has no method to maintain DMA on the proof code...
I think it's one of most difficult problems on proving code.

> In addition, List one of the other problems.
>
> * Time measurement and impatient interrupt
>
> When performing timing dependent processing, it is important to accurately know the current time.
> But ”time” has a nasty nature that will change as we measure.
> Also, we tend to think that execution time is predictable, but that is a big mistake.
> For example, A fickle compiler may put in a gap of our program one million nop instructions.
> Or more likely, long time interrupt handling may be inserted immediately after acquiring the current time, and the "current time" of that interrupt may be ruined.
> Temporary interrupt disabled will solve the problem of interrupts, but that's the entrance to another difficulty.

I also it's a hard for ATS compiler. ATS only maintains C code level design.
The seL4's approach may be useful for you.

https://ts.data61.csiro.au/publications/nicta_full_text/9118.pdf

But please remember it needs much human resource.

[Fujii Ken-ichi]

Hi Okabe.

2017年9月2日土曜日 18時05分00秒 UTC+9 Kiwamu Okabe:

Hi Fujii,

On Thu, Aug 31, 2017 at 1:58 PM, Fujii Ken-ichi <fuji...@gmail.com> wrote:
> If you are saying things like a register that can read an uncertain value unless some setting is made.
> So, I think there are two choices.
>
> 1.Restrict reading of registers.
>
>   Add arguments of the configuration view to the register read function.
>
> 2.Restrict　the use of reading results.
>
>  Add a snapshot of the setting view at the time of reading to the register view.
>
> Either way, I think that we should respond individually.

If we have HDL codes under the hardware registers, can we capture the
invariant as ATS proofs?

 

I do not know much about HDL, but I will answer.

First, I think it is difficult with classical HDL (VHDL and Verilog HDL).
It would be like doing the same thing from assembler code to retrieve the ATS certificate from those HDLs.

However, there is an extended language of HDL called PSL (Property Specification Language). It may be possible if it is used to describe HDL (and properly proved).

 

>> * Enforce that code doesn't start DMA without setup of buffer
>
> I think DMA will be a problem in programming with theorem-proving.
> Simplest solution is to prohibit DMA. Then we can put troubles in the trash box with usefulness.
>
> Even if you take other methods, DMA should not be applicable to all addresses.
> For example, it limits the read address of DMA to the receive register of the serial driver. In that case, the serial driver must also be designed to support DMA.
>
> Or perhaps it is better to give up on implementation at the driver level for DMA and provide only abstract interface.
>
> My recommendation is the first one.

I heard seL4 also has no method to maintain DMA on the proof code...
I think it's one of most difficult problems on proving code.

> In addition, List one of the other problems.
>
> * Time measurement and impatient interrupt
>
> When performing timing dependent processing, it is important to accurately know the current time.
> But ”time” has a nasty nature that will change as we measure.
> Also, we tend to think that execution time is predictable, but that is a big mistake.
> For example, A fickle compiler may put in a gap of our program one million nop instructions.
> Or more likely, long time interrupt handling may be inserted immediately after acquiring the current time, and the "current time" of that interrupt may be ruined.
> Temporary interrupt disabled will solve the problem of interrupts, but that's the entrance to another difficulty.

I also it's a hard for ATS compiler. ATS only maintains C code level design.
The seL4's approach may be useful for you.

https://ts.data61.csiro.au/publications/nicta_full_text/9118.pdf

But please remember it needs much human resource.

I did not know that seL4. It looks interesting, but it looks tough.
(But, how does this guarantee the real-time performance when the program prohibits interrupts ...?)
Thank you for telling me. I will learn it a little more.

 

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

 Thank you,