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 > <javascript:>> 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, -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/69fb0766-05e5-4dbb-81fa-f7ed73d9a7b8%40googlegroups.com.
