From: Simon Wright <simon@pushface.org>
Subject: Re: Advice, tasking and hardware
Date: Thu, 26 May 2016 09:13:53 +0100
Date: 2016-05-26T09:13:53+01:00 [thread overview]
Message-ID: <lyoa7tqlry.fsf@pushface.org> (raw)
In-Reply-To: ni5i6c$a2u$1@dont-email.me
"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> writes:
>> Spark doesn't use tasking, are there many dangers in using tasking
>> with hardware?
>
> SPARK 2014 includes Ravenscar
> tasking. (http://docs.adacore.com/spark2014-docs/html/lrm/tasks-and-synchronization.html)
But SPARK GPL 2015 doesn't support tasking. We live in hope that SPARK
GPL 2016 will.
I'm not sure of the best way to delegate tasking to the non-SPARK part
of a program while maintaining SPARK for as much as possible. I suppose
you'd have to be very restrained in your use of tasking (e.g. perhaps
only use Ravenscar tasking, have the task call a SPARK subprogram to do
the work).
I had a program with a large PO/task job dispatcher with multiple
entries and requeues in the PO, which was hugely improved when I had to
reimplement under Ravenscar.
next prev parent reply other threads:[~2016-05-26 8:13 UTC|newest]
Thread overview: 33+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-05-25 21:24 Advice, tasking and hardware patrick
2016-05-26 1:09 ` Jeffrey R. Carter
2016-05-26 8:13 ` Simon Wright [this message]
2016-05-26 7:26 ` Dmitry A. Kazakov
2016-05-26 16:41 ` patrick
2016-05-26 17:56 ` Dmitry A. Kazakov
2016-05-26 20:35 ` Jeffrey R. Carter
2016-05-26 19:35 ` Jeffrey R. Carter
2016-05-26 20:51 ` patrick
2016-05-27 7:50 ` Dmitry A. Kazakov
2016-05-27 18:00 ` Simon Wright
2016-05-27 19:06 ` Jeffrey R. Carter
2016-05-27 22:05 ` Randy Brukardt
2016-05-27 23:09 ` Jeffrey R. Carter
2016-05-27 19:13 ` Shark8
2016-05-27 20:27 ` Dmitry A. Kazakov
2016-05-27 22:27 ` Randy Brukardt
2016-05-28 6:49 ` Dmitry A. Kazakov
2016-05-28 14:38 ` Shark8
2016-05-28 15:45 ` Dmitry A. Kazakov
2016-05-28 0:25 ` rieachus
2016-05-28 1:57 ` patrick
2016-05-28 4:13 ` Jeffrey R. Carter
2016-06-01 14:37 ` rieachus
2016-06-01 19:09 ` Dmitry A. Kazakov
2016-06-06 3:33 ` rieachus
2016-06-06 7:18 ` Dmitry A. Kazakov
2016-06-07 16:53 ` rieachus
2016-06-07 20:21 ` Dmitry A. Kazakov
2016-06-08 4:06 ` rieachus
2016-06-08 7:29 ` Dmitry A. Kazakov
2016-06-08 12:56 ` rieachus
2016-06-08 0:19 ` Dennis Lee Bieber
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox