ATS for Linux kernel programming

Google Group
1

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:

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

2

I think you watch the repo. GitHub - metasepi/linux-bohai-s1: Linux Bohai - Season 1

Looks great! I will join you later.

Umm… I’ll use a real hardware. :wink:

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

Cheers!On Wednesday, October 22, 2014 1:52:08 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Wed, Oct 22, 2014 at 3:37 AM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

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

I think you watch the repo. GitHub - metasepi/linux-bohai-s1: Linux Bohai - Season 1

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. :wink:

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

3

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:

Index of /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.”

4

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.On Tuesday, October 21, 2014 2:37:35 PM UTC-4, gmhwxi wrote:

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.

5

This might be a useful tool, but I haven’t tried it:
http://snipersim.org/w/The_Sniper_Multi-Core_SimulatorOn Wednesday, 22 October 2014 14:23:26 UTC-4, gmhwxi wrote:

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.

On Tuesday, October 21, 2014 2:37:35 PM UTC-4, gmhwxi wrote:

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.

6

Here you can find the simplest kernel modules:

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:

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!

7

The Linux Kernel Module Programming Guide works

martinOn Thu, Nov 27, 2014 at 2:13 AM, ‘Yannick Duchêne’ via ats-lang-users ats-lan...@googlegroups.com wrote:

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.”

–
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.

8

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

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:

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 :slight_smile:

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!

–HongweiOn Friday, October 24, 2014 12:07:29 AM UTC-4, gmhwxi wrote:

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:

GitHub - githwxi/ATS-Postiats-contrib: ATS-Postiats-contrib is primarily for packages contributed to ATS-Postiats

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!

9

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]