ATS for Linux kernel programming

[gmhwxi]

Hi,

If you are reading this message, then you have probably heard or read that ATS
is good for safe systems programming. But you may not have seen low-level systems
code written in ATS, right? There is a reason for this obvious irony for writing such code
in ATS is very challenging. It took us a long time to learn the ropes.

Now I want to write a little bit on how ATS can be used effectively to implement low-level
systems. My focus here is on implementing device drivers for Linux. I will try to follow the
following book:

http://www.tldp.org/LDP/lkmpg/2.6/

The code I use is to be stored at:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/LinuxKerneling/

For testing, I suggest that a qemu image be used. I will do a post on it later.

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Oct 22, 2014 at 3:37 AM, gmhwxi <gmh...@gmail.com> wrote:
> https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/LinuxKerneling/

I think you watch the repo. https://github.com/metasepi/linux-bohai-s1

> For testing, I suggest that a qemu image be used. I will do a post on it
> later.

Umm.. I'll use a real hardware. ;)

Thank's,
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

>>I think you watch the repo. https://github.com/metasepi/linux-bohai-s1

Looks great!  I will join you later.

>>Umm.. I'll use a real hardware. ;)

Yes, real hardware, eventually. For now, my focus is on documenting and teaching.
I will first set things up (especially, headers files).

Cheers!

[Kiwamu Okabe]

Hi Hongwei,

On Thu, Oct 23, 2014 at 3:05 AM, gmhwxi <gmh...@gmail.com> wrote:
>>>I think you watch the repo. https://github.com/metasepi/linux-bohai-s1
>
> Looks great! I will join you later.

Today, I hosted kernel building on Travis-CI. It includes ATS2.

https://travis-ci.org/metasepi/linux-bohai-s1/

My next action is setup build environment for first Snatch.

>>>Umm.. I'll use a real hardware. ;)
>
> Yes, real hardware, eventually. For now, my focus is on documenting and
> teaching.
> I will first set things up (especially, headers files).

You are right.
Education is very important. And Raspberry PI is not good for it...

However, please know about qemu sometimes doesn't kick the kernel's
interrupt handler.
It's cheating and bad for debugging the kernel.

[gmhwxi]

>>However, please know about qemu sometimes doesn't kick the kernel's
>>interrupt handler.

Yes. I was also told to use Bochs. But Qemu is already very slow on my machine.

[Barry Schwartz]

gmhwxi <gmh...@gmail.com> skribis:

> Now I want to write a little bit on how ATS can be used effectively to
> implement low-level
> systems. My focus here is on implementing device drivers for Linux.

What I’d like to see is a GNU Hurd that doesn’t frequently
self-destruct, but indeed just days ago we had a Linux that
occasionally self-destructs, and that is far more important. :)

[Kiwamu Okabe]

Hi Barry,

On Thu, Oct 23, 2014 at 1:52 PM, Barry Schwartz
<chemoe...@chemoelectric.org> wrote:
> What I’d like to see is a GNU Hurd that doesn’t frequently
> self-destruct, but indeed just days ago we had a Linux that
> occasionally self-destructs, and that is far more important. :)

You are right.
How about think:

> After Linux kernel is perfectly rewritten with ATS2,
> it's easy to restructure monolithic kernel to monolithic kernel,
> little by little.

Then, I would like to focus "Linux kernel is perfectly rewritten with ATS2."

[Barry Schwartz]

Kiwamu Okabe <kiw...@debian.or.jp> skribis:

> How about think:
>
> > After Linux kernel is perfectly rewritten with ATS2,
> > it's easy to restructure monolithic kernel to monolithic kernel,
> > little by little.

That’s a special case of the observation everyone makes after they
learn an ML or such: changes tend to work the first time they pass
typechecking. But most such languages are no good for Linux kernel
work.

[Kiwamu Okabe]

Hi Barry,

On Thu, Oct 23, 2014 at 4:05 PM, Barry Schwartz
<chemoe...@chemoelectric.org> wrote:
> That’s a special case of the observation everyone makes after they
> learn an ML or such: changes tend to work the first time they pass
> typechecking. But most such languages are no good for Linux kernel
> work.

You are right.
Then, I try to rewrite everything. ;)

http://www.metasepi.org/

Regards,

[gmhwxi]

 
Here you can find the simplest kernel modules:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/LinuxKerneling/TEST/mycode/hello

The most important thing here is the way in which Makefile is written:

######

EXTRA_CFLAGS += -D_ATS_CCOMP_HEADER_NONE

EXTRA_CFLAGS += -D_ATS_CCOMP_PRELUDE_NONE

EXTRA_CFLAGS += -D_ATS_CCOMP_PRELUDE_USER=\"linux/H/pats_ccomp.h\"

EXTRA_CFLAGS += -D_ATS_CCOMP_EXCEPTION_NONE

######

EXTRA_CFLAGS += -I${PATSHOMERELOC}/contrib

###### The 'NONE' flags are needed to ensure that NO header files generated by the compiler are to be included. Instead, the following header file is used: ${PATSHOMERELOC}/contrib/linux/H/pats_ccomp.h If you want to try the code, then please make sure that you first git-clone the following package: https://github.com/githwxi/ATS-Postiats-contrib Then set PATSHOMERELOC to be the name of the directory containing the above package. For the rest, you just need to follow what is said in the book: http://www.tldp.org/LDP/lkmpg/2.6/ Please feel free to raise your questions here. I plan to implement a simple  char driver next time. Cheers!

[gmhwxi]

Okay, I managed to write a simple char driver in ATS:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/LinuxKerneling/TEST/mycode/chardev/chardev-1.dats

The code largely follows a corresponding example in

http://www.tldp.org/LDP/lkmpg/2.6/

but it works with Linux-3.0.

The primary difficulty here lies in setting up the necessary environment for Linux kernel programming:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/linux
https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/kernelats

I feel that this is like the ultimate test for any language attempting to support low-level systems programming.
It is actually a lot more difficult than writing an operating system in the tested language directly because interacting
with Linux kernel code requires a tremendously complex API. Not for faint-hearted :)

For the next example, my plan is to implement the SCULL character driver in the following book:

http://lwn.net/Kernel/LDD3/

As there is a bit algorithmic content in this driver, we should be able to see more interesting use of ATS.

Cheers!

--Hongwei

[gmhwxi]

I added chardev-2 to show how to implement 'write' operation.

Here are some command-lines that you can use to test chardev-1
and chardev-2:

#
# How to test chardev-1?
# (Testing other chardev-? is similar)
#

###### beg of [README] ######

Assume that you are in THIS directory.
Please issuing the following command-lines:

# for building kernel modules
make

# for inserting module
sudo insmod ./chardev-1_dats.ko

# for the assigned major number:
sudo fgrep -i chardev /var/log/messages

# assume the major number is xyz
# create a char device for testing
sudo mknod /dev/chardev-1 c xyz 0

# so device is writable for anyone
sudo chmod 666 /dev/chardev-1

# read from device
cat /dev/chardev-1

# write to device
# (chardev-1 not supporting write)
# (but chardev-2 does support write)
echo "Hello" > /dev/chardev-1

# for removing device
sudo rm /dev/chardev-1

# for removing module
sudo rmmod chardev-1_dats

###### end of [README] ######

[Yannick Duchêne]

Le mardi 21 octobre 2014 20:37:35 UTC+2, gmhwxi a écrit :

Hi,

If you are reading this message, then you have probably heard or read that ATS
is good for safe systems programming. But you may not have seen low-level systems
code written in ATS, right? There is a reason for this obvious irony for writing such code
in ATS is very challenging. It took us a long time to learn the ropes.

Now I want to write a little bit on how ATS can be used effectively to implement low-level
systems. My focus here is on implementing device drivers for Linux. I will try to follow the
following book:

http://www.tldp.org/LDP/lkmpg/2.6/

[…]

The link seems broken, I get a “You don't have permission to access /LDP/lkmpg/2.6/ on this server.” 

[Martin DeMello]

http://www.tldp.org/LDP/lkmpg/2.6/html/index.html works

martin

> --
> 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.
> Visit this group at http://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/6e07f458-a27e-42c1-80c7-ae57ad21329f%40googlegroups.com.

[Brandon Barker]

This might be a useful tool, but I haven't tried it: http://snipersim.org/w/The_Sniper_Multi-Core_Simulator