GPIO toggling with Xenomai

Hi folks.
I have a db410c with xenomai patched kernel. I’m trying to compare the performance of a RT task vs non RT one. For that purpose I have an osciloscope to which I connect one of the GPIOs (lets say 13 for example) and toggling it each second.
I wrote a code that creates a regular thread that executes a simple function that runs in a while loop for 10 sec and toggling the gpio13 port. Something like that:
void *reg_func()
{
time_t t = time(NULL) + 10;
while (time(NULL) < t) {
fprintf(val, “%d”, 1);
sleep(1);
fprintf(val, “%d”, 0);
sleep(1);
}
return NULL;
}

(Note: the fd of val in the code above is /sys/class/gpio/gpio13/value)

Before running that I’m running these command in the shell:
echo 13 > /sys/class/gpio/export
chmod ugo+rw /sys/class/gpio/gpio13/direction
echo out > /sys/class/gpio/gpio13/direction
chmod ugo+rw /sys/class/gpio/gpio13/value

I ran this code connected to the osciloscope and it works perfectly and does change the value.
Then I tried the same with a RT xenomai thread. I wrote something very similar to this:
http://www.armadeus.org/wiki/index.php?title=Xenomai:Blinking_LEDs
Of course I changed
#define LED “/dev/gpio/PD31”
to
#define GPIO_13 “/sys/class/gpio/gpio13/value”
and I expected it to do the same like the regular linux thread, but unfortunately it doesn’t work, and doesn’t even change the value at all. Also I’m not sure this is the right way to make a xenomai RT task toggle the GPIO. It’s really important that the RT task will use its RT abilities like using the ipipe and all this staff, to really feel the difference between the two tasks. Is this the right way to use that? and if does, what am I doing wrong?

Thanks.