Binary semaphore problem

I'm not sure if you want hints in how to prove a solution is correct, or if you want strategies for solving problems so I'll provide both.

I believe your approach is reasonable, but not complete. A good way to model synchronization problems is to think of how people behave (e.g. think of how 3 people would share 2 computers). People form queues -- a good way to avoid starvation; people are also able to look first then do (ie they do not have to commit to a course of action) and this is a good way to avoid deadlocks.

Validating that critical sections are not violated should not be too challenging for this case.

For deadlock you probably want to consider two types of cases: can two processes make a grab for a resource and end up with neither receiving it, and can a process requesting a resource prevent another from releasing a resource? Also, in small cases you can probably just consider all possible execution paths.

Also, don't forget to test for starvation. From what I remember you are usually allowed to assume that processes execute at a non-zero speed but with semaphores you are not guaranteed that the first process to wait will be the first to be signalled.

I'm not sure if you want more detail, but from what you said I would rather add more later if you want it. Also, sorry if some of this is just restating stuff you already know.

I would suggest using non-binary semaphores..
that is you create a semaphore with value equal to how many resources you have.
Then you can simply lock it..

You need to make sure that the locked processes are put in a queue on the semaphore, to prevent starvation.

/Nico

I'm reminded of semaphore problem on a university exam involving barbers which i'll adapt to get explain a possible approach.

You have a barber shop, with two barbers and one bench.
If a barber has no customers he's sleeping
If a barber has a customer he's working.
If a barber has no customers and one is waiting on the bench the customer moves to the barber and the barber is working.
If a customer comes in and a barber is sleeping the customer goes and wakes up the barber.
If a customer comes in and both barbers are working then they sit and wait on the bench.

Does looking at your problem and the possibles states for customers and barbers this way help?

Aly - I know how to prove if a solution is correct, but I feel like I'm gonna have to go through a tedious trial and error process of proving mutual exclusion/absence of deadlock/absence of starvation for a large number of permutations for each attempt at the solution. As for queuing, that will be provided intrinsically by the semaphore implementation, thus guaranteeing fairness. The 'look before doing' concept... that was what my overall semaphore was for, to guarantee exclusive access to the current state of the resources before making a decision to ask for one. Maybe the principles from Dekker's algorithm could be applied here, but that was ugly when generalised for 3 processes and 1 resource. No idea if it's even practical for 3 processes and 2 resources.

NicoDeLuciferi - As I said, I have no choice over the use of binary semaphores. In theory I could simulate a counting semaphore with binary ones but I was under the impression that this is a long-winded approach, and still doesn't solve the problem entirely as I still have to decide which of the 2 resources will be given to a requesting process.

TechnoGoth - The 'Sleeping Barber Problem' (not one that was covered on my course, incidentally) is the closest match I could find online before posting this. Unfortunately I can't see exactly how it maps onto my problem - do I have 2 barbers? If so, how do I know which one to 'wake up' without risking waiting forever on Barber 1 while Barber 2 sits idle? That's really the crux of the issue I think. I can't add any extra processes to mediate between the others.

You have to prove it won't deadlock or starve? Sounds like they want you to solve the halting problem.

Quite the opposite, in fact; these processes are potentially going to run forever. I just have to prove that the resources get allocated appropriately and exclusively when requested.

Alright,
but you can fairly simply implement counting semaphores using binary.
By just using 2 semaphores and an integer. But as you said it doesn't
solve your problem entirely.

/Nico

You don't say what operations you have on the semaphores and what restrictions there are... For instance can a process release a semaphore when it wasn't the one that acquired it in the first place (I'm assuming yes)? Can you atomically acquire both semaphores at once (I'm assuming no)?

Anyway, my hint is that the solution I came up with used one semaphore to protect the critical piece of information and the other to minimize the amount of time a process spends spinning.

The semaphores are essentially just global booleans, and I get atomic signal and wait instructions to call upon them. Those are the only atomic instructions guaranteed to be available.

My current attempted solution looks like this:


arbitrationSemaphore is used as a global lock for the 2 readerNFree variables to ensure they're only altered just after a reader finishes its task, and not between a writer seeing that one of them is true and setting off the appropriate process. The readerN_Start variables are there so that the readers aren't busy-waiting.

Can anyone see any obvious errors with this before I go down the formal verification route?

Your writer busy-waits if there are no free resources.

Can you reverse the problem?

Instead of giving the producer processes the job of waiting for the consumers to be free, can you give the consumers the job of linking with the next available producer as soon as the consumer is ready for more data?



Disclaimer: I haven't had formal training in this stuff; I'm probably missing something very obvious.

John B

AnonMike: I can cope with a little busy-waiting ;) As long as the other conditions are met, it's the lesser of 2 evils. Once it's working I can probably add in another semaphore there which wakes up the writer threads when the readers/resources signal it. Which seems to lead to what JohnBSmall said...

JohnBSmall: I sort of see where you're coming from, but I have no high-level list structure to work with, only the implied queuing that comes from waiting on a semaphore, which makes it a bit more difficult to picture mentally.

Do you know anything about the implementation of your semaphores? What I am wondering is can you be sure that if writer A does signal(arbitrationSemaphore) will that guarantee that if writer B performed a wait(arbitrationSemaphore) earlier will writer B be woken up? If not there might be a chance that writer A can sneak back into line and possibly reacquire the semaphore before writer B.

Also, for doing the analysis you can simplify it a bit by only considering two processes. This will catch most of the problems and you don't have to worry about riduculous numbers of permutations. Of course this wouldn't hold for a formal proof.

I am led to believe that the semaphores have a FIFO implementation for determining which process to resume, and that resuming such processes happens immediately if one is waiting. I think it's a reasonable assumption to work with anyway. This is more a theoretical exercise than a practical one.

Quote:

Original post by Kylotan JohnBSmall: I sort of see where you're coming from, but I have no high-level list structure to work with, only the implied queuing that comes from waiting on a semaphore, which makes it a bit more difficult to picture mentally.

My main reasoning was that since you have more producers than consumers, there will always be a producer sitting idle; that gives you an easy way to solve your problem of choosing couplings between producers and consumers - whenever a consumer finishes its job, it can be coupled with the producer that was idle.
That should also share the consumers evenly between producers, since the producers will each be activated in turn.

As regards using a list structure, obviously you can get the same effect in a number of ways using lower level primitives.

Which part are you having difficulty picturing?

John B

Quote:

Original post by JohnBSmall My main reasoning was that since you have more producers than consumers, there will always be a producer sitting idle; that gives you an easy way to solve your problem of choosing couplings between producers and consumers - whenever a consumer finishes its job, it can be coupled with the producer that was idle.

The problem there is that there's no guarantee that the idle producer is going to actually produce any time soon. If you assume that all producers produce at about the same rate and very often, this isn't a problem, but if you generalise it to any frequency and taking any finite length of time, it's no good. The consumer can't make any assumptions on which producer will produce next.

Quote:

As regards using a list structure, obviously you can get the same effect in a number of ways using lower level primitives.

Obviously it's possible to implement any sort of data structure out of the basics, but I get the impression that such a thing would be missing the point of the exercise, since the semaphores already provide their own queueing implementation. So it's to be done implicitly (by the order in which processes use 'wait' on a semaphore) rather than by placing anything into an explicit queue or list.

Quote:

Original post by Kylotan The problem there is that there's no guarantee that the idle producer is going to actually produce any time soon. If you assume that all producers produce at about the same rate and very often, this isn't a problem, but if you generalise it to any frequency and taking any finite length of time, it's no good. The consumer can't make any assumptions on which producer will produce next.

Ah, ok - I wasn't sure whether to assume that or not.

John B

Well, I seem to have come up with an algorithm that works in practice; the only problem is, I've just realised that we were never taught how to prove the correctness of a system that uses semaphores. :) Doh.

Quote:

TechnoGoth - The 'Sleeping Barber Problem' (not one that was covered on my course, incidentally) is the closest match I could find online before posting this. Unfortunately I can't see exactly how it maps onto my problem - do I have 2 barbers? If so, how do I know which one to 'wake up' without risking waiting forever on Barber 1 while Barber 2 sits idle? That's really the crux of the issue I think. I can't add any extra processes to mediate between the others.

well I'm sure there are lots of fancy ways you could do it but why not like this:



I'd help you with proving your algorithim works, but I long ago forgot how to do that. :)