# ATS for Linux kernel programming

**URL:** <https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533>\
**Category:** Google Group\
**Created:** [October 21, 2014, 6:37pm UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533 "2014-10-21T18:37:34Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 21, 2014, 6:37pm UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/1 "2014-10-21T18:37:34Z")

</div>

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/](http://www.tldp.org/LDP/lkmpg/2.6/)

The code I use is to be stored at:

> **[githwxi/ATS-Postiats-contrib](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/LinuxKerneling/)**
>
> ATS-Postiats-contrib is primarily for packages contributed to ATS-Postiats - githwxi/ATS-Postiats-contrib

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 22, 2014, 6:05pm UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/2 "2014-10-22T18:05:22Z")

</div>

> > I think you watch the repo. [GitHub - metasepi/linux-bohai-s1: Linux Bohai - Season 1](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!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](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > 
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/LinuxKerneling/](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](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

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [November 27, 2014, 10:13am UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/3 "2014-11-27T10:13:48Z")

</div>

> 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/](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.”

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 22, 2014, 6:23pm UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/4 "2014-10-22T18:23:26Z")

</div>

> > 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/](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/](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.

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker1](https://avatars.discourse-cdn.com/v4/letter/b/6a8cbe/32.png) [@Brandon\_Barker1](https://discourse.ats-lang.org/u/Brandon_Barker1)\
**Post date:** [February 23, 2015, 2:59pm UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/5 "2015-02-23T14:59:49Z")

</div>

This might be a useful tool, but I haven’t tried it:  
[http://snipersim.org/w/The\_Sniper\_Multi-Core\_SimulatorOn](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/](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/](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.

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 24, 2014, 4:07am UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/6 "2014-10-24T04:07:29Z")

</div>

Here you can find the simplest kernel modules:

> **[githwxi/ATS-Postiats-contrib](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/LinuxKerneling/TEST/mycode/hello)**
>
> ATS-Postiats-contrib is primarily for packages contributed to ATS-Postiats - githwxi/ATS-Postiats-contrib

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:

> **[githwxi/ATS-Postiats-contrib](https://github.com/githwxi/ATS-Postiats-contrib)**
>
> ATS-Postiats-contrib is primarily for packages contributed to ATS-Postiats - 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/](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!

---

<div class="post-metadata">

**Author:** ![Martin\_DeMello](https://avatars.discourse-cdn.com/v4/letter/m/f17d59/32.png) [@Martin\_DeMello](https://discourse.ats-lang.org/u/Martin_DeMello)\
**Post date:** [November 27, 2014, 10:33am UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/7 "2014-11-27T10:33:58Z")

</div>

[The Linux Kernel Module Programming Guide](http://www.tldp.org/LDP/lkmpg/2.6/html/index.html) works

martinOn Thu, Nov 27, 2014 at 2:13 AM, ‘Yannick Duchêne’ via ats-lang-users [ats-lan...@googlegroups.com](mailto: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/](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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/6e07f458-a27e-42c1-80c7-ae57ad21329f%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 28, 2014, 6:01pm UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/8 "2014-10-28T18:01:29Z")

</div>

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/](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>
>
> //github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/linux

> <https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/kernelats>
>
> //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/](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](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](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/](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!

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 31, 2014, 3:54am UTC](https://discourse.ats-lang.org/t/ats-for-linux-kernel-programming/533/9 "2014-10-31T03:54:56Z")

</div>

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]
