Deklarationen in atomic-Blöcken

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Deklarationen in atomic-Blöcken

Beitrag von null »

Hallo zusammen,

könnte mir jemand erklären, warum ich Deklarationen von Variablen nicht in atomic-Blöcke schreiben darf?

Vielen Dank

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Deklarationen in atomic-Blöcken

Beitrag von yourmaninamsterdam »

Das hat nicht unbedingt was mit atomic-Blöcken zu tun, sondern damit, dass Promela Deklarationen immer an den Beginn der Prozesse schiebt. Meines Erachtens lohnt es sich nicht wirklich, sich zu fragen, warum oder ob das toll ist, sondern man muss einfach damit leben.

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Deklarationen in atomic-Blöcken

Beitrag von null »

Aber es gibt ja konkrete Unterschiede. Schau dir mal diesen Code an:

Code: Alles auswählen

byte b = 0;

proctype P(){
	atomic{
		byte tmp = b;		//Ohne den atomic-Block käme es zu Verschränkungen
		tmp++;
		b = tmp;
	}
}


init {
	run P();
	run P();
	(_nr_pr == 1) -> assert (b ==2 );
}
Hier ist das assert nicht true, obwohl die die Anweisungen in einem atomic-Block stehen. Damit die Aussage in assert wahr wird, muss ich folgendes schreiben:

Code: Alles auswählen

byte tmp = 0;
atomic {
            tmp = b;
//...


Warum gibt es diesen doch sehr großen Unterschied?
Danke!

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Deklarationen in atomic-Blöcken

Beitrag von yourmaninamsterdam »

Das ändert ja nichts daran, dass es genaugenommen unzulässig ist, Deklarationen von Variablen nicht zu Beginn des Prozesses zu machen. Ich halte es zwar für eine schlechte Idee, das so zu handhaben, wie Promela das macht, nämlich über die Unzulässigkeit zu schweigen und irgendwelche Anweisungen zu verschieben, aber das tut ja für den konkreten Fall nichts zur Sache. Wenn du in deinem Beispiel die Deklaration 'byte tmp = b;' gedanklich an den Anfang des Prozesses verschiebst (was ja beim Ausführen auf die ein oder andere Weise geschieht), dann siehst du auch, warum das assert am Ende nicht unbedingt stimmt.

Die Essenz hier muss einfach sein: Richtig programmieren, also Deklarationen immer am Anfang, dann klappt es auch mit den asserts.

Antworten

Zurück zu „Archiv“