ATS programing on ChibiOS/RT and Arduino

[Kiwamu Okabe]

Hi all.

Second trying is ATS programing on ChibiOS/RT and Arduino.

https://github.com/fpiot/chibios-ats

ChibiOS/RT is very small RTOS that has good API.

http://www.chibios.org/dokuwiki/doku.php
http://chibios.sourceforge.net/html/index.html

ATS application source code is found at following.

https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/main.dats#L7

But it has some C language code yet...
I would like to have no more C code!!!

Do you have any idea?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

First, some minor issues:

you can write 1000u or 1000U for i2u(1000).

Also, I suggest

abst@ype SerialDriver = $extype"SerialDriver"

Then SerialDriver_p can be replaced with cPtr1(SerialDriver) (or cPtr0(SerialDriver)).

[Kiwamu Okabe]

Hi Hongwei.

On Fri, May 9, 2014 at 11:16 PM, gmhwxi <gmh...@gmail.com> wrote:
> you can write 1000u or 1000U for i2u(1000).
>
> Also, I suggest
>
> abst@ype SerialDriver = $extype"SerialDriver"
>
> Then SerialDriver_p can be replaced with cPtr1(SerialDriver) (or
> cPtr0(SerialDriver)).

The code is more readable.
I should learn linear type...

Thank's for your advice.

[gmhwxi]

I also suggest the following style of sequencing:

val () = do_this (...)
val () = do_that (...)

This style will make it very easy to add proofs into your code.

By the way, people often criticize the syntax of ATS for being verbose.
But in this case, the above style of sequencing is a lot more flexible than
the following very restricted form:

do_this (...); do_that (...);

For instance, we can later add proofs as follows:

val (pf | ()) = do_this (...)
val ((*void*)) = do_that (pf | ...)

[Kiwamu Okabe]

Hi Hongwei.

On Sat, May 10, 2014 at 1:16 AM, gmhwxi <gmh...@gmail.com> wrote:
> I also suggest the following style of sequencing:
>
> val () = do_this (...)
> val () = do_that (...)
>
> This style will make it very easy to add proofs into your code.
>
> By the way, people often criticize the syntax of ATS for being verbose.
> But in this case, the above style of sequencing is a lot more flexible than
> the following very restricted form:
>
> do_this (...); do_that (...);

I like OCaml style. But...

> For instance, we can later add proofs as follows:
>
> val (pf | ()) = do_this (...)
> val ((*void*)) = do_that (pf | ...)

It makes sense.
"When in Rome, do as the Romans do."


Thank's,

[gmhwxi]

When I see the following code:

do_this(...); do_that(...);

My first question is always: Why can't we write

do_that(...); do_this(...);

To many people, this sounds like a "stupid" question. But if you think
about it, this is actually a very profound question.

In Ocaml, this question is ignored. In other words, this question
can only be answered externally.

In Haskell, monads are introduced to support sequencing.

In ATS, you can think that the following code:

do_this (...); do_that (...);

is actually the erasure of

val (pf | ()) = do_this (...)
val ((*void*)) = do_that (pf | ...)

Clearly, we cannot call 'do_that' first because 'do_that'
needs a proof returned by a call to 'do_this'. This explains why,
sometimes, sequencing order, is significant (and, sometimes, it
is insignificant).

[john skaller]

On 10/05/2014, at 3:04 AM, gmhwxi wrote:
>
> is actually the erasure of
>
> val (pf | ()) = do_this (...)
> val ((*void*)) = do_that (pf | ...)
>
> Clearly, we cannot call 'do_that' first because 'do_that'
> needs a proof returned by a call to 'do_this'. This explains why,
> sometimes, sequencing order, is significant (and, sometimes, it
> is insignificant).

And when it is insignificant and we can evaluate in parallel,
how is that indicated?

--
john skaller
ska...@users.sourceforge.net
http://felix-lang.org

[gmhwxi]

In ATS, a pure function can write but it can only write
to the memory it owns. The design in ATS goes like this:

If I want to indicate to the compiler that that do_this and do_that
can be evaluated in parallel, I use the following syntax:

prval (pf1, pf2) = ... // [pf1] and [pf2] are separated
val ... = do_this (pf1 | ...) // do_this is checked to be pure
and ... = do_that (pf2 | ...) // do_that is checked to be pure

Basically, the requirement is that (1) do_this and do_that can
only manipulate resources they own and (2) they do not share
any resources between them.

[john skaller]

On 10/05/2014, at 10:24 AM, gmhwxi wrote:

>
> In ATS, a pure function can write but it can only write
> to the memory it owns. The design in ATS goes like this:
>
> If I want to indicate to the compiler that that do_this and do_that
> can be evaluated in parallel, I use the following syntax:
>
> prval (pf1, pf2) = ... // [pf1] and [pf2] are separated
> val ... = do_this (pf1 | ...) // do_this is checked to be pure
> and ... = do_that (pf2 | ...) // do_that is checked to be pure
>
> Basically, the requirement is that (1) do_this and do_that can
> only manipulate resources they own and (2) they do not share
> any resources between them.

Ah yes of course, this is the standard ML notation.
I wonder, however, if you can also do this:

val (), () = f1 a1, f2 a2

[omitting proofs]

BTW: it isn't necessary that two procedures not modify shared
memory to use them in parallel. A simple example, they both
do atomic increments on a shared variable. Clearly the procedures
aren't pure, in fact no procedures can possibly be pure or they
would be worthless.

If you consider two processes modifying separate files,
clearly each has side effects, and it looks like these procedures
are independent. But this is NOT the case in the larger picture,
they're both modifying files in a single file system.

So the separation requirement is a fallacy: in its simple form
it is worthless. Clearly the real requirement is that some
invariant be satisfied "at some time in the future".

So actually I'd expect some form like:

prval (psync) = .. with
prval (pf1, pf2) =
..

where the psync is the synchronisation proof, and the individual proofs
pf1 and pf2 may take the synchronisation proof's conclusion as a premise.
[Or did I get this backwards .. lets see]

Roughly, if f1 and f2 each add 1 to a shared variable, then provided
addition is atomic, we can deduce that after both f1 and f2 have completed
the variable will be two greater.

But basically my point is: for functions purity or whatever may be useful
because the *system* manages the assignment of their result values
in some fixed specified way. Technically these are procedures with
side effects, and in general, procedures ALWAYS have side effects
because they don't return values and would be useless if they
didn't have side effects.

So functions are really procedures with system specified
side effects and a system invariant. Its a special case.

[gmhwxi]

Whether a function is pure or not depends on the
underlying (abstract) model for computation. At the
machine-level, computation cannot be pure. For instance,
evaluation of pure functions in Haskell certainly generates
a lot of effects at run-time.

I have repeatedly read arguments by ML people claiming that
Haskell functions are not really pure. But these arguments
do not make much sense; whether a Haskell function is pure or
not should be judged in the Haskell's model for computation (
assuming that the model can be correctly implemented at machine-level
).

In ATS, pure functions can acquire locks and can atomically
increment a shared variable. The programmer has the ultimate
say as to whether an operation is pure or not. We have to have
such kind of flexibility to support practical programming.

>>If you consider two processes modifying separate files,
>>clearly each has side effects, and it looks like these procedures
>>are independent. But this is NOT the case in the larger picture,
>>they're both modifying files in a single file system.

Maybe the notion of file system does not exist in my model for
computation. It is entirely possible that files will have different
time stamps based on different evaluation order, but this may not
be part of the model used to judge the purity of the two processes.

>>But basically my point is: for functions purity or whatever may be useful
>>because the *system* manages the assignment of their result values
>>in some fixed specified way. Technically these are procedures with
>>side effects, and in general, procedures ALWAYS have side effects
>>because they don't return values and would be useless if they
>>didn't have side effects.

Yes, if you talk about purity at machine-level. Only proof functions
are pure at that level :)

[Kiwamu Okabe]

Hi all.

Remaining C language source code on following.

https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/main.dats

```
%{^
#include "ch.h"
#include "hal.h"
#include "test.h"
%}

%{
static WORKING_AREA(waThread1, 32);

msg_t thread1_ats(void *);
void c_entry(void) {
/* Starts the LED blinker thread. */
chThdCreateStatic(waThread1, sizeof(waThread1), NORMALPRIO,
thread1_ats, NULL);
}
%}
```

How to pass ATS envless function (thread1) pointer to C language
function (chThdCreateStatic)?

Thank's,

[Kiwamu Okabe]

Yeahhhhhhhhhh, I got it!

On Sat, May 10, 2014 at 3:31 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/main.dats
> --snip--

> How to pass ATS envless function (thread1) pointer to C language
> function (chThdCreateStatic)?

Now we have only following C code on the application.

%{^
#include "ch.h"
#include "hal.h"
#include "test.h"
%}

%{
static WORKING_AREA(waThread1, 32);

%}

I think it's not logic, that is simple data structure.

[Kiwamu Okabe]

Hi Hongwei.

BTW.
The ccomp/runtime/pats_ccomp_typedefs.h file has a big array.

```ats
// HX: making it not usable!!!
//
typedef
struct{char _[0XFFFF];} atstype_var[0] ;
```

64KiB is too big for 8-bit or 16-bit microcontroller.
# Sometime 32-bit arch also: LPC812M101JDH20 :: NXP
# http://www.nxp.com/products/microcontrollers/cortex_m0_m0/lpc800/LPC812M101JDH20.html

I have escaped it with dirty hack.

https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/Makefile#L639

```makefile
pats_ccomp_typedefs.h:
sed -e 's/_\[0XFFFF\]/_\[0X00FF\]/g' ${PATSHOME}/ccomp/runtime/$@ > $@
```

Is it needed for ATS language today?

[Hongwei Xi]

atstype_var is not supposed to be used by the compiler.

I have now introduced a flag as follows to control its size:

//
// HX-2014-05:
// making it not usable!!!
//
#ifndef _ATSTYPE_VAR_SIZE
#define _ATSTYPE_VAR_SIZE 0X10000
#endif // end of [#ifndef]
//
// HX-2014-05:
// for 8-bit or 16-bit march,
// _ATSTYPE_VAR_SIZE can be set to 0x100
//
typedef
struct{char _[_ATSTYPE_VAR_SIZE];} atstype_var[0] ;
//

--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnEV7rwx9%2BFFFeuNV2zzJ6fkN%2BGeifRP9mv2pUojdoSUA%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei.

On Sun, May 11, 2014 at 1:01 AM, Hongwei Xi <gmh...@gmail.com> wrote:
> I have now introduced a flag as follows to control its size:

> --snip--

> #ifndef _ATSTYPE_VAR_SIZE
> #define _ATSTYPE_VAR_SIZE 0X10000
> #endif // end of [#ifndef]

I'll fix my Makefile when ats2-positiats-0.0.9 is released.

[john skaller]

On 10/05/2014, at 1:10 PM, Hongwei Xi wrote:

> I was intentionally vague about purity.

>
> Whether a function is pure or not depends on the
> underlying (abstract) model for computation.

Ok, I agree. I like your approach.
What you're doing with ATS is the biggest advance
in software development technology since Autocoder.

[Brandon Barker]

So I'm probably missing several points here, including how to properly use proofs and even what is meant by parallel. But I never saw any parallelism in these concrete examples:

(* ****** ****** *)
//
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)


%{^
  int do_adding() {
  volatile unsigned int i = 1;
  while(i >= 0) {
    i = i + 1;
  }
  return -1;
  }
%}




extern
fun do_adding():int = "mac#"
// Now with proofs:
dataprop TESTPROP =
  | TEST of ()
extern
fun do_adding_usepf(pf: TESTPROP | ):int = "mac#do_adding"
//




implement main0() = let


// val x = do_adding() and y = do_adding()
// same cpu usage as:
// val x = do_adding()


prval apf = TEST()
prval bpf = TEST()


// The cpu usage is the same again
val x = do_adding_usepf(apf | ) and y = do_adding_usepf(bpf | )


in
println!(x)
end

[Brandon Barker]

It seems that it would be a very convenient syntax. Anyone could make a simple wrapper function requiring a proof if they want to call something in a parallel context.

Brandon Barker
brandon...@gmail.com

On Sat, May 17, 2014 at 11:55 AM, gmhwxi <gmh...@gmail.com> wrote:

The compiler does to support it right now :)

--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com.

[gmhwxi]

This is parallel-let binding.

It was actually supported in ATS at one-point as an
experiment:

http://www.cs.bu.edu/~hwxi/academic/papers/sblp09.pdf