Lamport's bakery algorithm

Lamport's bakery algorithm is a computer algorithm devised by computer scientist Leslie Lamport, as part of his long study of the formal correctness of concurrent systems, which is intended to improve the safety in the usage of shared resources among multiple threads by means of mutual exclusion.

In computer science, it is common for multiple threads to simultaneously access the same resources. Data corruption can occur if two or more threads try to write into the same memory location, or if one thread reads a memory location before another has finished writing into it. Lamport's bakery algorithm is one of many mutual exclusion algorithms designed to prevent concurrent threads entering critical sections of code concurrently to eliminate the risk of data corruption.

Algorithm

Analogy

Lamport envisioned a bakery with a numbering machine at its entrance so each customer is given a unique number. Numbers increase by one as customers enter the store. A global counter displays the number of the customer that is currently being served. All other customers must wait in a queue until the baker finishes serving the current customer and the next number is displayed. When the customer is done shopping and has disposed of his or her number, the clerk increments the number, allowing the next customer to be served. That customer must draw another number from the numbering machine in order to shop again.

According to the analogy, the "customers" are threads, identified by the letter i, obtained from a global variable.

Due to the limitations of computer architecture, some parts of Lamport's analogy need slight modification. It is possible that more than one thread will get the same number n when they request it; this cannot be avoided (without first solving the mutual exclusion problem, which is the goal of the algorithm). Therefore, it is assumed that the thread identifier i is also a priority. A lower value of i means a higher priority and threads with higher priority will enter the critical section first.

Critical section

The critical section is that part of code that requires exclusive access to resources and may only be executed by one thread at a time. In the bakery analogy, it is when the customer trades with the baker that others must wait.

When a thread wants to enter the critical section, it has to check whether now is its turn to do so. It should check the number n of every other thread to make sure that it has the smallest one. In case another thread has the same number, the thread with the smallest i will enter the critical section first.

In pseudocode this comparison between threads a and b can be written in the form:

// Let na - the customer number for thread a, and
// ia - the thread number for thread a, then

(na, ia) < (nb, ib) 

which is equivalent to:

(na < nb) or ((na == nb) and (ia < ib))

Once the thread ends its critical job, it gets rid of its number and enters the non-critical section.

Non-critical section

The non-critical section is the part of code that doesn't need exclusive access. It represents some thread-specific computation that doesn't interfere with other threads' resources and execution.

This part is analogous to actions that occur after shopping, such as putting change back into the wallet.

Implementation of the algorithm

Definitions

In Lamport's original paper, the entering variable is known as choosing, and the following conditions apply:

  • Words choosing [i] and number [i] are in the memory of process i, and are initially zero.
  • The range of values of number [i] is unbounded.
  • A process may fail at any time. We assume that when it fails, it immediately goes to its noncritical section and halts. There may then be a period when reading from its memory gives arbitrary values. Eventually, any read from its memory must give a value of zero.

Code examples

Pseudocode

In this example, all threads execute the same "main" function, Thread. In real applications, different threads often have different "main" functions.

Note that as in the original paper, the thread checks itself before entering the critical section. Since the loop conditions will evaluate as false, this does not cause much delay.

  // declaration and initial values of global variables
  Entering: array [1..NUM_THREADS] of bool = {false};
  Number: array [1..NUM_THREADS] of integer = {0};

  lock(integer i) {
      Entering[i] = true;
      Number[i] = 1 + max(Number[1], ..., Number[NUM_THREADS]);
      Entering[i] = false;
      for (integer j = 1; j <= NUM_THREADS; j++) {
          // Wait until thread j receives its number:
          while (Entering[j]) { /* nothing */ }
          // Wait until all threads with smaller numbers or with the same
          // number, but with higher priority, finish their work:
          while ((Number[j] != 0) && ((Number[j], j) < (Number[i], i))) { /* nothing */ }
      }
  }
  
  unlock(integer i) {
      Number[i] = 0;
  }

  Thread(integer i) {
      while (true) {
          lock(i);
          // The critical section goes here...
          unlock(i);
          // non-critical section...
      }
  }

Each thread only writes its own storage, only reads are shared. It is remarkable that this algorithm is not built on top of some lower level "atomic" operation, e.g. compare-and-swap. The original proof shows that for overlapping reads and writes to the same storage cell only the write must be correct.[clarification needed] The read operation can return an arbitrary number. Therefore, this algorithm can be used to implement mutual exclusion on memory that lacks synchronisation primitives, e.g., a simple SCSI disk shared between two computers.

The necessity of the variable Entering might not be obvious as there is no 'lock' around lines 7 to 13. However, suppose the variable was removed and two processes computed the same Number[i]. If the higher-priority process was preempted before setting Number[i], the low-priority process will see that the other process has a number of zero, and enters the critical section; later, the high-priority process will ignore equal Number[i] for lower-priority processes, and also enters the critical section. As a result, two processes can enter the critical section at the same time. The bakery algorithm uses the Entering variable to make the assignment on line 6 look like it was atomic; process i will never see a number equal to zero for a process j that is going to pick the same number as i.

When implementing the pseudo code in a single process system or under cooperative multitasking, it is better to replace the "do nothing" sections with code that notifies the operating system to immediately switch to the next thread. This primitive is often referred to as yield.

Lamport's bakery algorithm assumes a sequential consistency memory model. Few, if any, languages or multi-core processors implement such a memory model. Therefore, correct implementation of the algorithm typically requires inserting fences to inhibit reordering.[1]

PlusCal code

We declare N to be the number of processes, and we assume that N is a natural number.

CONSTANT N
ASSUME N \in Nat

We define P to be the set {1, 2, ... , N} of processes.

P == 1..N

The variables num and flag are declared as global.

--algorithm AtomicBakery {
variable num = [i \in P |-> 0], flag = [i \in P |-> FALSE];

The following defines LL(j, i) to be true iff <<num[j], j>> is less than or equal to <<num[i], i>> in the usual lexicographical ordering.

define { LL(j, i) == \/ num[j] < num[i]
                     \/ /\ num[i] = num[j]
                        /\ j =< i
       }

For each element in P there is a process with local variables unread, max and nxt. Steps between consecutive labels p1, ..., p7, cs are considered atomic. The statement with (x \in S) { body } sets id to a nondeterministically chosen element of the set S and then executes body. A step containing the statement await expr can be executed only when the value of expr is TRUE.

process (p \in P)
  variables unread \in SUBSET P, 
            max \in Nat, 
            nxt \in P;
{
p1: while (TRUE) {
      unread := P \ {self} ;
      max := 0;
      flag[self] := TRUE;
p2:   while (unread # {}) {
        with (i \in unread) { unread := unread \ {i};
                              if (num[i] > max) { max := num[i]; }
         }
       };
p3:   num[self] := max + 1;
p4:   flag[self] := FALSE;
      unread := P \ {self} ;
p5:   while (unread # {}) {
        with (i \in unread) { nxt := i ; };
        await ~ flag[nxt];
p6:     await \/ num[nxt] = 0
              \/ LL(self, nxt) ;
        unread := unread \ {nxt};
        } ;
cs:   skip ;  \* the critical section;
p7:   num[self] := 0;
 }}
}

Java code

We use the AtomicIntegerArray class not for its built in atomic operations but because its get and set methods work like volatile reads and writes. Under the Java Memory Model this ensures that writes are immediately visible to all threads.

AtomicIntegerArray ticket = new AtomicIntegerArray(threads); // ticket for threads in line, n - number of threads
// Java initializes each element of 'ticket' to 0
 
AtomicIntegerArray entering = new AtomicIntegerArray(threads); // 1 when thread entering in line
// Java initializes each element of 'entering' to 0
 
public void lock(int pid) // thread ID
{
    entering.set(pid, 1);
    int max = 0;
    for (int i = 0; i < threads; i++)
    {
        int current = ticket.get(i);
        if (current > max)
        {
            max = current;
        }
    }
    ticket.set(pid, 1 + max); 
    entering.set(pid, 0);
    for (int i = 0; i < ticket.length(); ++i)
    {
        if (i != pid)
        {
            while (entering.get(i) == 1) { Thread.yield(); } // wait while other thread picks a ticket
            while (ticket.get(i) != 0 && ( ticket.get(i) < ticket.get(pid) ||
                    (ticket.get(i) == ticket.get(pid) && i < pid)))
            { Thread.yield(); }
        }
    }
    // The critical section goes here...
}

public void unlock(int pid)
{
    ticket.set(pid, 0);
}

See also

References

  1. ^ Chinmay Narayan, Shibashis Guha, S.Arun-Kumar Inferring Fences in a Concurrent Program Using SC proof of Correctness

Read other articles:

Winners of the Masters Tournament since 1934 Jack Nicklaus, six-time Masters champion in 1963, 1965, 1966, 1972, 1975, and 1986, which is a record, is one of three golfers to successfully defend his title. He is also one of five champions to win wire-to-wire, in 1972. The Masters Tournament is a golf competition that was established in 1934, with Horton Smith winning the inaugural tournament.[1] The Masters is the first of four major championships to be played each year, with the fina...

 

Artikel ini perlu dikembangkan agar dapat memenuhi kriteria sebagai entri Wikipedia.Bantulah untuk mengembangkan artikel ini. Jika tidak dikembangkan, artikel ini akan dihapus. Artikel ini tidak memiliki referensi atau sumber tepercaya sehingga isinya tidak bisa dipastikan. Tolong bantu perbaiki artikel ini dengan menambahkan referensi yang layak. Tulisan tanpa sumber dapat dipertanyakan dan dihapus sewaktu-waktu.Cari sumber: Dok maritim – berita · surat kabar ...

 

Daulat Agung Utsmaniyahدولت عليه عثمانیه Devlet-i ʿAlīye-i ʿOsmānīye1299–1923 Bendera Lambang Semboyan: Devlet-i Ebed-müddetدولت ابد مدتNegara AbadiJangkauan terluas Kesultanan Utsmaniyah tahun 1683Wilayah Utsmaniyah (merah) bersama negara vasal (merah terang) Kesultanan Utsmaniyah abad ke-16.StatusImperiumIbu kotaSöğüt(1299–1335)Bursa[1](1335–1413)Adrianopel[2][dn 1](1413–1453)Konstantinopel[dn 2](1453–1922)Baha...

قرية أنثورب الإحداثيات 44°12′00″N 75°37′00″W / 44.2°N 75.6167°W / 44.2; -75.6167  [1] تقسيم إداري  البلد الولايات المتحدة[2]  التقسيم الأعلى مقاطعة جيفيرسون  خصائص جغرافية  المساحة 2.674223 كيلومتر مربع2.763975 كيلومتر مربع (1 أبريل 2010)  ارتفاع 156 متر  عدد السكان &...

 

Republic Records Empresa matriz Universal Music GroupFundación 1995Fundador(es) Monte LipmanAvery LipmanDistribuidor Universal Music Group, Virgin EMI Records / Island Records y Universal Music EnterprisesGénero(s) VariosPaís Estados UnidosLocalización Ciudad de Nueva York, Nueva YorkGrupo Universal Music LatinUMG RecordingsWeb oficial[editar datos en Wikidata] Republic Records es un sello discográfico estadounidense que opera como una división de Universal Music Group. El sel...

 

Aaron pada tahun 1978. Henry Louis Hank Aaron (5 Februari 1934 – 22 Januari 2021) adalah seorang pemain bisbol Amerika Serikat yang aktif dari tahun 1950-an hingga 1970-an. Ia terkenal sebagai pemain dengan rekor home run terbanyak di Major League Baseball (sebanyak 755) hingga rekor tersebut dipecahkan Barry Bonds pada tahun 2007 setelah 33 tahun. Rekor Aaron sendiri memecahkan rekor sebelumnya yang dipegang Babe Ruth. Berposisi sebagai outfielder, Aaron memperkuat tim Milwau...

Dan AttiasDan Attias pada 2011Lahir04 Desember 1951 (umur 72)Los Angeles, CaliforniaPekerjaanSutradara televisi, produser televisiTahun aktif1978–sekarangSuami/istriDiane AttiasAnakDavid AttiasRachel Attias Daniel Attias (lahir 4 Desember 1951)[1] adalah seorang produser dan sutradara televisi asal Amerika Serikat. Attias berkarier selama tiga dekade, di mana ia menyutradarai sejumlah program televisi waktu perdana populer, yang meliputi Miami Vice dan Beverly Hills, 9021...

 

Priest of Rome elected pope in March 752 In sources prior to the 1960s, this pope is called Stephen II and Pope Stephen II is called Stephen III. Pope-electStephenPredecessorZacharySuccessorStephen II (as Pope) Celestine II (as Pope-elect)OrdersCreated cardinal745by ZacharyPersonal detailsBornRomeDied(752-03-25)25 March 752RomePrevious post(s)Cardinal-priest of San Crisogono (745–752)Other popes named Stephen Pope-elect Stephen (died 25 March 752) was a Roman priest selected in March 7...

 

هذه المقالة تحتاج للمزيد من الوصلات للمقالات الأخرى للمساعدة في ترابط مقالات الموسوعة. فضلًا ساعد في تحسين هذه المقالة بإضافة وصلات إلى المقالات المتعلقة بها الموجودة في النص الحالي. (ديسمبر 2018) مقاطعة روزبود     الإحداثيات 46°14′N 106°43′W / 46.23°N 106.72°W / 46.23; -106...

Collège d'AlbionHistoireFondation 1835StatutType Université privéeNom officiel Albion CollegeRégime linguistique anglaisPrésident Donna M. RandallDevise Lux Fiat (« que la lumière soit »)Membre de American Council on Education (en)Site web www.albion.eduChiffres-clésÉtudiants 1950Effectif 499 (2020)LocalisationPays États-UnisCampus urbainVille Albion, MichiganLocalisation sur la carte du MichiganLocalisation sur la carte des États-Unismodifier - modifier le code - modifi...

 

Alioum Saidou Nazionalità  Camerun Altezza 181 cm Calcio Ruolo Centrocampista Termine carriera 2011 - giocatore Carriera Giovanili 1995-1997 Cotonsport Garoua Squadre di club1 1997-1999 Cotonsport Garoua? (?)1999-2004 İstanbulspor159 (12)2004-2005 Galatasaray6 (0)2005→  Malatyaspor13 (0)2005-2006 Galatasaray23 (0)2006-2007 Nantes-Atlantique32 (0)2007-2010 Kayserispor79 (6)2010-2011 Sivasspor4 (0) Nazionale 1997-2009 Camerun13 (4) Carriera...

 

Classified United States government satellite ZumaLaunch by SpaceX of the Zuma satelliteNames USA-280[1] Mission 1390[2] Mission typeMilitary (classified)OperatorNorthrop Grumman, for the U.S. government[3]COSPAR ID2018-001A SATCAT no.43098 Spacecraft propertiesManufacturerNorthrop Grumman Start of missionLaunch date8 January 2018, 01:00 (2018-01-08UTC01) UTC[1]RocketFalcon 9 Full ThrustLaunch siteCape Canaveral, SLC-40ContractorSpaceX End of missionD...

هذه المقالة يتيمة إذ تصل إليها مقالات أخرى قليلة جدًا. فضلًا، ساعد بإضافة وصلة إليها في مقالات متعلقة بها. (فبراير 2016) بعثة الأمم المتحدة للمراقبة في اليمنمعلومات عامةصنف فرعي من منظمة أسستها الأمم المتحدة البداية يونيو 1963 الاسم الرسمي United Nations Yemen Observation Mission (بالإنجليزية) ا...

 

Sean P. Maloney Anggota Dewan Perwakilan Rakyat A.S.dari dapil Ke-18 New YorkPetahanaMulai menjabat 3 Januari 2013PendahuluNan Hayworth (Pembagian Wilayah)PenggantiPetahanaKantor Staf Sekretaris di Gedung PutihMasa jabatan1999–2000PresidenBill ClintonPendahuluPhillip CaplanPenggantiLisel Loy Informasi pribadiLahirSean Patrick Maloney30 Juli 1966 (umur 57)Sherbrooke, Quebec, KanadaPartai politikDemokratSuami/istriRandy Florke ​(m. 2014)​Anak3...

 

Maltese manager and former footballer (born 1970) Oliver Spiteri Personal informationFull name Oliver SpiteriDate of birth (1970-07-04) 4 July 1970 (age 53)Place of birth Attard, MaltaHeight 5 ft 10 in (1.78 m)Position(s) Midfielder[1]Senior career*Years Team Apps (Gls)1986–1990 Birkirkara 1990–1997 St. Lucia 1997–1998 Żabbar St. Patrick's 1998–2000 Birkirkara 1998–2000 Lija Athletic Managerial career2003–2004 Birkirkara U162004–2005 Birkirkara U1920...

Voce principale: UYBA Volley. Futura Volley Busto ArsizioStagione 2008-2009Sport pallavolo Squadra Busto Arsizio Allenatore Carlo Parisi All. in seconda Mariela Codaro Presidente Michele Forte Serie A14ª Play-off scudettoSemifinali Coppa ItaliaSemifinali Maggiori presenzeCampionato: Borri, Campanari, Ferreira, Matuszková, Viganò (32)Totale: Borri, Campanari, Ferreira, Matuszková, Viganò (38) Miglior marcatoreCampionato: Loikkanen (440)Totale: Loikkanen (532) 2007-08 2009-10 Questa ...

 

Statue of Li Kui Part of a series onChinese legalism Figures Guan Zhong Marquess Wen of Wei Li Kui Duke Xiao of Qin Shang Yang Shen Buhai Wu Qi Shen Dao Zhang Yi Han Fei Li Si Qin Shi Huang Han figures Jia Yi Emperor Wen of Han Emperor Wu of Han Chao Cuo Gongsun Hong Zhang Tang Huan Tan Wang Fu Zhuge Liang Later figures Emperor Wen of Sui Du You Wang Anshi Li Shanchang Zhang Juzheng Xu Guangqi Relevant texts Guanzi The Book of Lord Shang Shenzi (both books) Han Feizi Wuzi Wei Liaozi Annals of...

 

Process of obtaining intravenous access Drawing blood redirects here. For the book, see Drawing Blood. Still photo of a venipuncture procedure Video of a venipuncture procedure In medicine, venipuncture or venepuncture is the process of obtaining intravenous access for the purpose of venous blood sampling (also called phlebotomy) or intravenous therapy. In healthcare, this procedure is performed by medical laboratory scientists, medical practitioners, some EMTs, paramedics, phlebotomists, dia...

vteCranleigh line Legend Portsmouth Direct line North Downs Lineto Reading New Guildford line Guildford Guildford Tunnel(833 yd, 762 m) St Catherine's Hill Tunnel(133 yd, 122 m) Shalford Junction North Downs Lineto Redhill and Gatwick Airport Portsmouth Direct lineto Portsmouth Peasmarsh Junction River Wey Bramley & Wonersh Cranleigh Portsmouth lineto Dorking and Leatherhead Baynards Arun Valley line Bay...

 

Когда два или более сейсмометров обнаруживают Р-волны (вверху), JMA анализирует показания и распределяет предупреждающую информацию, транслируемую станциями и компаниями мобильной связи, до прихода S-волн (внизу). Общенациональная система раннего предупреждения о землет�...