Hi Fujii, On Thu, Aug 31, 2017 at 1:58 PM, Fujii Ken-ichi <fujiik...@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. Best regards, -- Kiwamu Okabe at METASEPI DESIGN -- 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/CAEvX6dmJxn8-fJup8S7AkdSR4Q6xTXBXCQndsnhSnkTOFAd1ag%40mail.gmail.com.
